4atlem12

Description: Lemma for 4at . Combine all four possible cases. (Contributed by NM, 11-Jul-2012)

	Ref	Expression
Hypotheses	4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	4at.j	$⊢ \underset{˙}{\lor} = join (K)$
	4at.a	$⊢ A = Atoms (K)$
Assertion	4atlem12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Proof

Step	Hyp	Ref	Expression
1		4at.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		4at.j	$⊢ \underset{˙}{\lor} = join (K)$
3		4at.a	$⊢ A = Atoms (K)$
4		simpl11	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in HL$
5	4	hllatd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to K \in Lat$
6		simpl12	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in A$
7		eqid	$⊢ {Base}_{K} = {Base}_{K}$
8	7 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
9	6 8	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \in {Base}_{K}$
10		simpl13	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to Q \in A$
11	7 3	atbase	$⊢ Q \in A \to Q \in {Base}_{K}$
12	10 11	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to Q \in {Base}_{K}$
13		simpl23	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to T \in A$
14		simpl31	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to U \in A$
15	7 2 3	hlatjcl	$⊢ (K \in HL \land T \in A \land U \in A) \to T \underset{˙}{\lor} U \in {Base}_{K}$
16	4 13 14 15	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to T \underset{˙}{\lor} U \in {Base}_{K}$
17		simpl32	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to V \in A$
18		simpl33	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to W \in A$
19	7 2 3	hlatjcl	$⊢ (K \in HL \land V \in A \land W \in A) \to V \underset{˙}{\lor} W \in {Base}_{K}$
20	4 17 18 19	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to V \underset{˙}{\lor} W \in {Base}_{K}$
21	7 2	latjcl	$⊢ (K \in Lat \land T \underset{˙}{\lor} U \in {Base}_{K} \land V \underset{˙}{\lor} W \in {Base}_{K}) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
22	5 16 20 21	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K}$
23	7 1 2	latjle12	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
24	5 9 12 22 23	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
25		simpl21	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in A$
26	7 3	atbase	$⊢ R \in A \to R \in {Base}_{K}$
27	25 26	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \in {Base}_{K}$
28		simpl22	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in A$
29	7 3	atbase	$⊢ S \in A \to S \in {Base}_{K}$
30	28 29	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to S \in {Base}_{K}$
31	7 1 2	latjle12	$⊢ (K \in Lat \land (R \in {Base}_{K} \land S \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
32	5 27 30 22 31	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
33	24 32	anbi12d	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
34		simpl1	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land P \in A \land Q \in A)$
35	7 2 3	hlatjcl	$⊢ (K \in HL \land P \in A \land Q \in A) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
36	34 35	syl	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to P \underset{˙}{\lor} Q \in {Base}_{K}$
37	7 2 3	hlatjcl	$⊢ (K \in HL \land R \in A \land S \in A) \to R \underset{˙}{\lor} S \in {Base}_{K}$
38	4 25 28 37	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to R \underset{˙}{\lor} S \in {Base}_{K}$
39	7 1 2	latjle12	$⊢ (K \in Lat \land (P \underset{˙}{\lor} Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K} \land (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W) \in {Base}_{K})) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
40	5 36 38 22 39	syl13anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land (R \underset{˙}{\lor} S) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
41	33 40	bitrd	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \leftrightarrow ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
42		simp1l	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
43		simp1r	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
44		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
45		simp3	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
46	1 2 3	4atlem12b	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R)) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
47	42 43 44 45 46	syl121anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
48	47	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
49	7 2	latj4rot	$⊢ (K \in Lat \land (Q \in {Base}_{K} \land R \in {Base}_{K}) \land (S \in {Base}_{K} \land P \in {Base}_{K})) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} P) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
50	5 12 27 30 9 49	syl122anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} P) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
51	50	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} P) = (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)$
52	4 10 25	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land Q \in A \land R \in A)$
53	28 6 13	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \in A \land P \in A \land T \in A)$
54		simpl3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (U \in A \land V \in A \land W \in A)$
55	52 53 54	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((K \in HL \land Q \in A \land R \in A) \land (S \in A \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
56	55	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((K \in HL \land Q \in A \land R \in A) \land (S \in A \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
57		simpr	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))$
58	1 2 3	4noncolr3	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
59	34 25 28 57 58	syl121anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
60	59	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S))$
61		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
62		simprlr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
63		simprrl	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
64	62 63	jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
65		simprrr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
66		simprll	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
67	64 65 66	jca32	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
68	67	3adant2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
69	1 2 3	4atlem12b	$⊢ (((K \in HL \land Q \in A \land R \in A) \land (S \in A \land P \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((Q \neq R \land \neg S \underset{˙}{\leq} (Q \underset{˙}{\lor} R) \land \neg P \underset{˙}{\leq} ((Q \underset{˙}{\lor} R) \underset{˙}{\lor} S)) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} P) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
70	56 60 61 68 69	syl121anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (Q \underset{˙}{\lor} R) \underset{˙}{\lor} (S \underset{˙}{\lor} P) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
71	51 70	eqtr3d	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
72	71	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
73	48 72	jaod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
74	7 2	latjcom	$⊢ (K \in Lat \land P \underset{˙}{\lor} Q \in {Base}_{K} \land R \underset{˙}{\lor} S \in {Base}_{K}) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
75	5 36 38 74	syl3anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
76	75	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (R \underset{˙}{\lor} S) \underset{˙}{\lor} (P \underset{˙}{\lor} Q)$
77	4 25 28	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land R \in A \land S \in A)$
78	6 10 13	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \in A \land Q \in A \land T \in A)$
79	77 78 54	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((K \in HL \land R \in A \land S \in A) \land (P \in A \land Q \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
80	79	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((K \in HL \land R \in A \land S \in A) \land (P \in A \land Q \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
81	1 2 3	4noncolr2	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P))$
82	34 25 28 57 81	syl121anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P))$
83	82	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P))$
84		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
85		simprr	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
86		simprl	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
87	85 86	jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
88	87	3adant2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
89	1 2 3	4atlem12b	$⊢ (((K \in HL \land R \in A \land S \in A) \land (P \in A \land Q \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((R \neq S \land \neg P \underset{˙}{\leq} (R \underset{˙}{\lor} S) \land \neg Q \underset{˙}{\leq} ((R \underset{˙}{\lor} S) \underset{˙}{\lor} P)) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (R \underset{˙}{\lor} S) \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
90	80 83 84 88 89	syl121anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (R \underset{˙}{\lor} S) \underset{˙}{\lor} (P \underset{˙}{\lor} Q) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
91	76 90	eqtrd	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
92	91	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
93	7 2	latj4rot	$⊢ (K \in Lat \land (P \in {Base}_{K} \land Q \in {Base}_{K}) \land (R \in {Base}_{K} \land S \in {Base}_{K})) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
94	5 9 12 27 30 93	syl122anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
95	94	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R)$
96	4 28 6	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (K \in HL \land S \in A \land P \in A)$
97	10 25 13	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (Q \in A \land R \in A \land T \in A)$
98	96 97 54	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((K \in HL \land S \in A \land P \in A) \land (Q \in A \land R \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
99	98	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((K \in HL \land S \in A \land P \in A) \land (Q \in A \land R \in A \land T \in A) \land (U \in A \land V \in A \land W \in A))$
100	1 2 3	4noncolr1	$⊢ ((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q))$
101	34 25 28 57 100	syl121anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q))$
102	101	3ad2ant1	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q))$
103		simp2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)$
104	65 66	jca	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
105	104 62 63	jca32	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
106	105	3adant2	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to ((S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))$
107	1 2 3	4atlem12b	$⊢ (((K \in HL \land S \in A \land P \in A) \land (Q \in A \land R \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land ((S \neq P \land \neg Q \underset{˙}{\leq} (S \underset{˙}{\lor} P) \land \neg R \underset{˙}{\leq} ((S \underset{˙}{\lor} P) \underset{˙}{\lor} Q)) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \land ((S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
108	99 102 103 106 107	syl121anc	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (S \underset{˙}{\lor} P) \underset{˙}{\lor} (Q \underset{˙}{\lor} R) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
109	95 108	eqtrd	$⊢ ((((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \land \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \land ((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)$
110	109	3exp	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (\neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
111	92 110	jaod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))$
112	25 28 14	3jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (R \in A \land S \in A \land U \in A)$
113	17 18	jca	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (V \in A \land W \in A)$
114	1 2 3	4atlem3	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land U \in A) \land (V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \lor (\neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)))$
115	34 112 113 57 114	syl31anc	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to ((\neg P \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg Q \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)) \lor (\neg R \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W) \lor \neg S \underset{˙}{\leq} ((U \underset{˙}{\lor} V) \underset{˙}{\lor} W)))$
116	73 111 115	mpjaod	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (((P \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land Q \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))) \land (R \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \land S \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)))) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$
117	41 116	sylbird	$⊢ (((K \in HL \land P \in A \land Q \in A) \land (R \in A \land S \in A \land T \in A) \land (U \in A \land V \in A \land W \in A)) \land (P \neq Q \land \neg R \underset{˙}{\leq} (P \underset{˙}{\lor} Q) \land \neg S \underset{˙}{\leq} ((P \underset{˙}{\lor} Q) \underset{˙}{\lor} R))) \to (((P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S)) \underset{˙}{\leq} ((T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W)) \to (P \underset{˙}{\lor} Q) \underset{˙}{\lor} (R \underset{˙}{\lor} S) = (T \underset{˙}{\lor} U) \underset{˙}{\lor} (V \underset{˙}{\lor} W))$

Metamath Proof Explorer

Theorem 4atlem12

Proof