Theorem dalawlem15

Description: Lemma for dalaw . Swap variable triples P Q R and S T U in dalawlem14 , to obtain the elimination of the remaining conditions in dalawlem1 . (Contributed by NM, 6-Oct-2012)

	Ref	Expression
Hypotheses	dalawlem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	dalawlem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	dalawlem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
	dalawlem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	dalawlem2.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
Assertion	dalawlem15	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		dalawlem.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		dalawlem.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		dalawlem.m	$$⊢\underset{\dot{}}{\wedge }=\mathrm{meet}\left(K\right)$$
4		dalawlem.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
5		dalawlem2.o	$$⊢O=\mathrm{LPlanes}\left(K\right)$$
6		simp11	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to K\in \mathrm{HL}$$
7		simp12	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)$$
8		simp21	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to P\in A$$
9		simp31	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to S\in A$$
10	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge S\in A\right)\to P\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }P$$
11	6 8 9 10	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to P\underset{\dot{}}{\vee }S=S\underset{\dot{}}{\vee }P$$
12		simp22	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to Q\in A$$
13		simp32	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to T\in A$$
14	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge T\in A\right)\to Q\underset{\dot{}}{\vee }T=T\underset{\dot{}}{\vee }Q$$
15	6 12 13 14	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to Q\underset{\dot{}}{\vee }T=T\underset{\dot{}}{\vee }Q$$
16	11 15	oveq12d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)=\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)$$
17	16	breq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
18	17	notbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\leftrightarrow \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)$$
19	16	breq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
20	19	notbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\leftrightarrow \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
21	16	breq1d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)$$
22	21	notbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\leftrightarrow \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)$$
23	18 20 22	3anbi123d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\leftrightarrow \left(\neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)$$
24	23	anbi2d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\right)$$
25	7 24	mtbid	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)$$
26		simp13	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)$$
27	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge P\in A\right)\to S\underset{\dot{}}{\vee }P=P\underset{\dot{}}{\vee }S$$
28	6 9 8 27	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to S\underset{\dot{}}{\vee }P=P\underset{\dot{}}{\vee }S$$
29	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge T\in A\wedge Q\in A\right)\to T\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }T$$
30	6 13 12 29	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to T\underset{\dot{}}{\vee }Q=Q\underset{\dot{}}{\vee }T$$
31	28 30	oveq12d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)=\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)$$
32		simp33	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to U\in A$$
33		simp23	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to R\in A$$
34	2 4	hlatjcom	$$⊢\left(K\in \mathrm{HL}\wedge U\in A\wedge R\in A\right)\to U\underset{\dot{}}{\vee }R=R\underset{\dot{}}{\vee }U$$
35	6 32 33 34	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to U\underset{\dot{}}{\vee }R=R\underset{\dot{}}{\vee }U$$
36	26 31 35	3brtr4d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }R\right)$$
37		simp3	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(S\in A\wedge T\in A\wedge U\in A\right)$$
38		simp2	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(P\in A\wedge Q\in A\wedge R\in A\right)$$
39	1 2 3 4 5	dalawlem14	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(S\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }R\right)\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(\left(\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\vee }\left(\left(U\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }P\right)\right)\right)$$
40	6 25 36 37 38 39	syl311anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }Q\right)\right)\underset{\dot{}}{\le }\left(\left(\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\vee }\left(\left(U\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }P\right)\right)\right)$$
41	6	hllatd	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to K\in \mathrm{Lat}$$
42		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
43	42 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
44	6 8 12 43	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
45	42 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge T\in A\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
46	6 9 13 45	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
47	42 3	latmcom	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }Q\right)$$
48	41 44 46 47	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\wedge }\left(P\underset{\dot{}}{\vee }Q\right)$$
49	42 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge Q\in A\wedge R\in A\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
50	6 12 33 49	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
51	42 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge T\in A\wedge U\in A\right)\to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
52	6 13 32 51	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
53	42 3	latmcom	$$⊢\left(K\in \mathrm{Lat}\wedge Q\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)=\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }R\right)$$
54	41 50 52 53	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)=\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }R\right)$$
55	42 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge R\in A\wedge P\in A\right)\to R\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K$$
56	6 33 8 55	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to R\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K$$
57	42 2 4	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge U\in A\wedge S\in A\right)\to U\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
58	6 32 9 57	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to U\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K$$
59	42 3	latmcom	$$⊢\left(K\in \mathrm{Lat}\wedge R\underset{\dot{}}{\vee }P\in {\mathrm{Base}}_K\wedge U\underset{\dot{}}{\vee }S\in {\mathrm{Base}}_K\right)\to \left(R\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(U\underset{\dot{}}{\vee }S\right)=\left(U\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }P\right)$$
60	41 56 58 59	syl3anc	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(R\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(U\underset{\dot{}}{\vee }S\right)=\left(U\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }P\right)$$
61	54 60	oveq12d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(U\underset{\dot{}}{\vee }S\right)\right)=\left(\left(T\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }R\right)\right)\underset{\dot{}}{\vee }\left(\left(U\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(R\underset{\dot{}}{\vee }P\right)\right)$$
62	40 48 61	3brtr4d	$$⊢\left(\left(K\in \mathrm{HL}\wedge \neg \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in O\wedge \left(\neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(T\underset{\dot{}}{\vee }U\right)\wedge \neg \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)\wedge \left(\left(P\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\wedge }\left(Q\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(R\underset{\dot{}}{\vee }U\right)\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\wedge }\left(S\underset{\dot{}}{\vee }T\right)\right)\underset{\dot{}}{\le }\left(\left(\left(Q\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\wedge }\left(T\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\vee }\left(\left(R\underset{\dot{}}{\vee }P\right)\underset{\dot{}}{\wedge }\left(U\underset{\dot{}}{\vee }S\right)\right)\right)$$