Theorem oa8todual 971

Description: Conventional to dual 8-variable OA law. (Contributed by NM, 8-May-2000.)

Hypothesis

Ref	Expression
oa8to5.1	(((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))

Assertion

Ref	Expression
oa8todual	(b ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ ((e ∩ f) ∪ (g ∩ h)))

Proof of Theorem oa8todual

Step	Hyp	Ref	Expression
1		oa8to5.1	. . 3 (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))) ≤ (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))
2	1	lecon 154	. 2 (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))⊥ ≤ (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ )))⊥
3		ax-a1 30	. . . 4 b = b⊥ ⊥
4		ax-a1 30	. . . . . 6 a = a⊥ ⊥
5		ax-a1 30	. . . . . . . 8 c = c⊥ ⊥
6		df-a 40	. . . . . . . . . . . . . 14 (a ∩ c) = (a⊥ ∪ c⊥ )⊥
7		df-a 40	. . . . . . . . . . . . . 14 (b ∩ d) = (b⊥ ∪ d⊥ )⊥
8	6, 7	2or 72	. . . . . . . . . . . . 13 ((a ∩ c) ∪ (b ∩ d)) = ((a⊥ ∪ c⊥ )⊥ ∪ (b⊥ ∪ d⊥ )⊥ )
9		oran3 93	. . . . . . . . . . . . 13 ((a⊥ ∪ c⊥ )⊥ ∪ (b⊥ ∪ d⊥ )⊥ ) = ((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ ))⊥
10	8, 9	ax-r2 36	. . . . . . . . . . . 12 ((a ∩ c) ∪ (b ∩ d)) = ((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ ))⊥
11		df-a 40	. . . . . . . . . . . . . . . 16 (a ∩ g) = (a⊥ ∪ g⊥ )⊥
12		df-a 40	. . . . . . . . . . . . . . . 16 (b ∩ h) = (b⊥ ∪ h⊥ )⊥
13	11, 12	2or 72	. . . . . . . . . . . . . . 15 ((a ∩ g) ∪ (b ∩ h)) = ((a⊥ ∪ g⊥ )⊥ ∪ (b⊥ ∪ h⊥ )⊥ )
14		oran3 93	. . . . . . . . . . . . . . 15 ((a⊥ ∪ g⊥ )⊥ ∪ (b⊥ ∪ h⊥ )⊥ ) = ((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ ))⊥
15	13, 14	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∩ g) ∪ (b ∩ h)) = ((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ ))⊥
16		df-a 40	. . . . . . . . . . . . . . . 16 (c ∩ g) = (c⊥ ∪ g⊥ )⊥
17		df-a 40	. . . . . . . . . . . . . . . 16 (d ∩ h) = (d⊥ ∪ h⊥ )⊥
18	16, 17	2or 72	. . . . . . . . . . . . . . 15 ((c ∩ g) ∪ (d ∩ h)) = ((c⊥ ∪ g⊥ )⊥ ∪ (d⊥ ∪ h⊥ )⊥ )
19		oran3 93	. . . . . . . . . . . . . . 15 ((c⊥ ∪ g⊥ )⊥ ∪ (d⊥ ∪ h⊥ )⊥ ) = ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))⊥
20	18, 19	ax-r2 36	. . . . . . . . . . . . . 14 ((c ∩ g) ∪ (d ∩ h)) = ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))⊥
21	15, 20	2an 79	. . . . . . . . . . . . 13 (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h))) = (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ ))⊥ ∩ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))⊥ )
22		anor3 90	. . . . . . . . . . . . 13 (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ ))⊥ ∩ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))⊥ ) = (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))⊥
23	21, 22	ax-r2 36	. . . . . . . . . . . 12 (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h))) = (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))⊥
24	10, 23	2or 72	. . . . . . . . . . 11 (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) = (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ ))⊥ ∪ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))⊥ )
25		oran3 93	. . . . . . . . . . 11 (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ ))⊥ ∪ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))⊥ ) = (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))))⊥
26	24, 25	ax-r2 36	. . . . . . . . . 10 (((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) = (((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))))⊥
27		df-a 40	. . . . . . . . . . . . . . . 16 (a ∩ e) = (a⊥ ∪ e⊥ )⊥
28		df-a 40	. . . . . . . . . . . . . . . 16 (b ∩ f) = (b⊥ ∪ f⊥ )⊥
29	27, 28	2or 72	. . . . . . . . . . . . . . 15 ((a ∩ e) ∪ (b ∩ f)) = ((a⊥ ∪ e⊥ )⊥ ∪ (b⊥ ∪ f⊥ )⊥ )
30		oran3 93	. . . . . . . . . . . . . . 15 ((a⊥ ∪ e⊥ )⊥ ∪ (b⊥ ∪ f⊥ )⊥ ) = ((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ ))⊥
31	29, 30	ax-r2 36	. . . . . . . . . . . . . 14 ((a ∩ e) ∪ (b ∩ f)) = ((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ ))⊥
32		df-a 40	. . . . . . . . . . . . . . . . . 18 (e ∩ g) = (e⊥ ∪ g⊥ )⊥
33		df-a 40	. . . . . . . . . . . . . . . . . 18 (f ∩ h) = (f⊥ ∪ h⊥ )⊥
34	32, 33	2or 72	. . . . . . . . . . . . . . . . 17 ((e ∩ g) ∪ (f ∩ h)) = ((e⊥ ∪ g⊥ )⊥ ∪ (f⊥ ∪ h⊥ )⊥ )
35		oran3 93	. . . . . . . . . . . . . . . . 17 ((e⊥ ∪ g⊥ )⊥ ∪ (f⊥ ∪ h⊥ )⊥ ) = ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))⊥
36	34, 35	ax-r2 36	. . . . . . . . . . . . . . . 16 ((e ∩ g) ∪ (f ∩ h)) = ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))⊥
37	15, 36	2an 79	. . . . . . . . . . . . . . 15 (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))) = (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ ))⊥ ∩ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))⊥ )
38		anor3 90	. . . . . . . . . . . . . . 15 (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ ))⊥ ∩ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))⊥ ) = (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥
39	37, 38	ax-r2 36	. . . . . . . . . . . . . 14 (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))) = (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥
40	31, 39	2or 72	. . . . . . . . . . . . 13 (((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) = (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ ))⊥ ∪ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥ )
41		oran3 93	. . . . . . . . . . . . 13 (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ ))⊥ ∪ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥ ) = (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥
42	40, 41	ax-r2 36	. . . . . . . . . . . 12 (((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) = (((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥
43		df-a 40	. . . . . . . . . . . . . . . 16 (c ∩ e) = (c⊥ ∪ e⊥ )⊥
44		df-a 40	. . . . . . . . . . . . . . . 16 (d ∩ f) = (d⊥ ∪ f⊥ )⊥
45	43, 44	2or 72	. . . . . . . . . . . . . . 15 ((c ∩ e) ∪ (d ∩ f)) = ((c⊥ ∪ e⊥ )⊥ ∪ (d⊥ ∪ f⊥ )⊥ )
46		oran3 93	. . . . . . . . . . . . . . 15 ((c⊥ ∪ e⊥ )⊥ ∪ (d⊥ ∪ f⊥ )⊥ ) = ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ ))⊥
47	45, 46	ax-r2 36	. . . . . . . . . . . . . 14 ((c ∩ e) ∪ (d ∩ f)) = ((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ ))⊥
48	20, 36	2an 79	. . . . . . . . . . . . . . 15 (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))) = (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))⊥ ∩ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))⊥ )
49		anor3 90	. . . . . . . . . . . . . . 15 (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))⊥ ∩ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))⊥ ) = (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥
50	48, 49	ax-r2 36	. . . . . . . . . . . . . 14 (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))) = (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥
51	47, 50	2or 72	. . . . . . . . . . . . 13 (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) = (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ ))⊥ ∪ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥ )
52		oran3 93	. . . . . . . . . . . . 13 (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ ))⊥ ∪ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))⊥ ) = (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥
53	51, 52	ax-r2 36	. . . . . . . . . . . 12 (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) = (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥
54	42, 53	2an 79	. . . . . . . . . . 11 ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))) = ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥ ∩ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥ )
55		anor3 90	. . . . . . . . . . 11 ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥ ∩ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))⊥ ) = ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))⊥
56	54, 55	ax-r2 36	. . . . . . . . . 10 ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))) = ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))⊥
57	26, 56	2or 72	. . . . . . . . 9 ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))))) = ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))))⊥ ∪ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))⊥ )
58		oran3 93	. . . . . . . . 9 ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ ))))⊥ ∪ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))⊥ ) = ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))⊥
59	57, 58	ax-r2 36	. . . . . . . 8 ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))))) = ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))⊥
60	5, 59	2an 79	. . . . . . 7 (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))) = (c⊥ ⊥ ∩ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))⊥ )
61		anor3 90	. . . . . . 7 (c⊥ ⊥ ∩ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))⊥ ) = (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))⊥
62	60, 61	ax-r2 36	. . . . . 6 (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))) = (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))⊥
63	4, 62	2or 72	. . . . 5 (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))))))) = (a⊥ ⊥ ∪ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))⊥ )
64		oran3 93	. . . . 5 (a⊥ ⊥ ∪ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))⊥ ) = (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))))⊥
65	63, 64	ax-r2 36	. . . 4 (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))))))) = (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))))⊥
66	3, 65	2an 79	. . 3 (b ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))))) = (b⊥ ⊥ ∩ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))))⊥ )
67		anor3 90	. . 3 (b⊥ ⊥ ∩ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ ))))))))⊥ ) = (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))⊥
68	66, 67	ax-r2 36	. 2 (b ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))))) = (b⊥ ∪ (a⊥ ∩ (c⊥ ∪ ((((a⊥ ∪ c⊥ ) ∩ (b⊥ ∪ d⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )))) ∩ ((((a⊥ ∪ e⊥ ) ∩ (b⊥ ∪ f⊥ )) ∩ (((a⊥ ∪ g⊥ ) ∩ (b⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))) ∪ (((c⊥ ∪ e⊥ ) ∩ (d⊥ ∪ f⊥ )) ∩ (((c⊥ ∪ g⊥ ) ∩ (d⊥ ∪ h⊥ )) ∪ ((e⊥ ∪ g⊥ ) ∩ (f⊥ ∪ h⊥ )))))))))⊥
69		df-a 40	. . . . . 6 (a ∩ b) = (a⊥ ∪ b⊥ )⊥
70		df-a 40	. . . . . 6 (c ∩ d) = (c⊥ ∪ d⊥ )⊥
71	69, 70	2or 72	. . . . 5 ((a ∩ b) ∪ (c ∩ d)) = ((a⊥ ∪ b⊥ )⊥ ∪ (c⊥ ∪ d⊥ )⊥ )
72		oran3 93	. . . . 5 ((a⊥ ∪ b⊥ )⊥ ∪ (c⊥ ∪ d⊥ )⊥ ) = ((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ ))⊥
73	71, 72	ax-r2 36	. . . 4 ((a ∩ b) ∪ (c ∩ d)) = ((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ ))⊥
74		df-a 40	. . . . . 6 (e ∩ f) = (e⊥ ∪ f⊥ )⊥
75		df-a 40	. . . . . 6 (g ∩ h) = (g⊥ ∪ h⊥ )⊥
76	74, 75	2or 72	. . . . 5 ((e ∩ f) ∪ (g ∩ h)) = ((e⊥ ∪ f⊥ )⊥ ∪ (g⊥ ∪ h⊥ )⊥ )
77		oran3 93	. . . . 5 ((e⊥ ∪ f⊥ )⊥ ∪ (g⊥ ∪ h⊥ )⊥ ) = ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))⊥
78	76, 77	ax-r2 36	. . . 4 ((e ∩ f) ∪ (g ∩ h)) = ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))⊥
79	73, 78	2or 72	. . 3 (((a ∩ b) ∪ (c ∩ d)) ∪ ((e ∩ f) ∪ (g ∩ h))) = (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ ))⊥ ∪ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))⊥ )
80		oran3 93	. . 3 (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ ))⊥ ∪ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ ))⊥ ) = (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ )))⊥
81	79, 80	ax-r2 36	. 2 (((a ∩ b) ∪ (c ∩ d)) ∪ ((e ∩ f) ∪ (g ∩ h))) = (((a⊥ ∪ b⊥ ) ∩ (c⊥ ∪ d⊥ )) ∩ ((e⊥ ∪ f⊥ ) ∩ (g⊥ ∪ h⊥ )))⊥
82	2, 68, 81	le3tr1 140	1 (b ∩ (a ∪ (c ∩ ((((a ∩ c) ∪ (b ∩ d)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((c ∩ g) ∪ (d ∩ h)))) ∪ ((((a ∩ e) ∪ (b ∩ f)) ∪ (((a ∩ g) ∪ (b ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h)))) ∩ (((c ∩ e) ∪ (d ∩ f)) ∪ (((c ∩ g) ∪ (d ∩ h)) ∩ ((e ∩ g) ∪ (f ∩ h))))))))) ≤ (((a ∩ b) ∪ (c ∩ d)) ∪ ((e ∩ f) ∪ (g ∩ h)))

This proof depends on syntax axioms:   ≤ wle 2  ^⊥ wn 4   ∪ wo 6   ∩ wa 7

This proof depends on axioms:  ax-a1 30  ax-a2 31  ax-a5 34  ax-r1 35  ax-r2 36  ax-r4 37  ax-r5 38

This proof depends on definitions:  df-a 40  df-le1 130  df-le2 131

This theorem is used by:  oa8to5  972