Theorem 2lplnja

Description: The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj in terms of atoms). (Contributed by NM, 12-Jul-2012)

	Ref	Expression
Hypotheses	2lplnja.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	2lplnja.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
	2lplnja.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
	2lplnja.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
Assertion	2lplnja	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)=W$$

Proof

Step	Hyp	Ref	Expression
1		2lplnja.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
2		2lplnja.j	$$⊢\underset{\dot{}}{\vee }=\mathrm{join}\left(K\right)$$
3		2lplnja.a	$$⊢A=\mathrm{Atoms}\left(K\right)$$
4		2lplnja.v	$$⊢V=\mathrm{LVols}\left(K\right)$$
5		eqid	$$⊢{\mathrm{Base}}_K={\mathrm{Base}}_K$$
6		simp11l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to K\in \mathrm{HL}$$
7	6	hllatd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to K\in \mathrm{Lat}$$
8		simp121	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\in A$$
9		simp122	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to Q\in A$$
10	5 2 3	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$$
11	6 8 9 10	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K$$
12		simp123	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\in A$$
13	5 3	atbase	$$⊢R\in A\to R\in {\mathrm{Base}}_K$$
14	12 13	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to R\in {\mathrm{Base}}_K$$
15	5 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge P\underset{\dot{}}{\vee }Q\in {\mathrm{Base}}_K\wedge R\in {\mathrm{Base}}_K\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
16	7 11 14 15	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K$$
17		simp2l1	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\in A$$
18		simp2l2	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\in A$$
19	5 2 3	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$$
20	6 17 18 19	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K$$
21		simp2l3	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to U\in A$$
22	5 3	atbase	$$⊢U\in A\to U\in {\mathrm{Base}}_K$$
23	21 22	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to U\in {\mathrm{Base}}_K$$
24	5 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
25	7 20 23 24	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
26	5 2	latjcl	$$⊢\left(K\in \mathrm{Lat}\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K$$
27	7 16 25 26	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\in {\mathrm{Base}}_K$$
28		simp11r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to W\in V$$
29	5 4	lvolbase	$$⊢W\in V\to W\in {\mathrm{Base}}_K$$
30	28 29	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to W\in {\mathrm{Base}}_K$$
31		simp31	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W$$
32		simp32	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W$$
33	5 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\le }W\right)$$
34	7 16 25 30 33	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\le }W\right)$$
35	31 32 34	mpbi2and	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\underset{\dot{}}{\le }W$$
36	5 1 2	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\to U\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
37	7 20 23 36	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to U\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
38	5 1 7 23 25 30 37 32	lattrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to U\underset{\dot{}}{\le }W$$
39	5 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge U\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\right)$$
40	7 16 23 30 39	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge U\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\right)$$
41	31 38 40	mpbi2and	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W$$
42	41	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W$$
43	6	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to K\in \mathrm{HL}$$
44	6 8 9	3jca	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
45	44	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
46	12 21	jca	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(R\in A\wedge U\in A\right)$$
47	46	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(R\in A\wedge U\in A\right)$$
48		simp13l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to P\ne Q$$
49	48	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to P\ne Q$$
50		simp13r	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
51	50	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
52		simp33	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
53	52	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
54		simplr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
55		simpr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
56	5 3	atbase	$$⊢S\in A\to S\in {\mathrm{Base}}_K$$
57	17 56	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\in {\mathrm{Base}}_K$$
58	5 3	atbase	$$⊢T\in A\to T\in {\mathrm{Base}}_K$$
59	18 58	syl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\in {\mathrm{Base}}_K$$
60	5 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\in {\mathrm{Base}}_K\wedge T\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\right)\to \left(\left(S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
61	7 57 59 16 60	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
62	61	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
63	54 55 62	mpbi2and	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
64	63	adantr	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
65		simpr	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
66	5 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\underset{\dot{}}{\vee }T\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
67	7 20 23 16 66	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
68	67	ad3antrrr	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\leftrightarrow \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
69	64 65 68	mpbi2and	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
70		simp2l	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\in A\wedge T\in A\wedge U\in A\right)$$
71		simp12	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(P\in A\wedge Q\in A\wedge R\in A\right)$$
72		simp2rr	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)$$
73		simp2rl	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\ne T$$
74	1 2 3	3at	$$⊢\left(\left(K\in \mathrm{HL}\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)\wedge \left(\neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\wedge S\ne T\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
75	6 70 71 72 73 74	syl32anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
76	75	ad3antrrr	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\leftrightarrow \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
77	69 76	mpbid	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R$$
78	77	eqcomd	$$⊢\left(\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U$$
79	78	ex	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\to \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R=\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
80	79	necon3ad	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\to \neg U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)$$
81	53 80	mpd	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \neg U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
82	1 2 3 4	lvoli2	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge U\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg U\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\in V$$
83	45 47 49 51 81 82	syl113anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\in V$$
84	28	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\in V$$
85	1 4	lvolcmp	$$⊢\left(K\in \mathrm{HL}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\in V\wedge W\in V\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U=W\right)$$
86	43 83 84 85	syl3anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U=W\right)$$
87	42 86	mpbid	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U=W$$
88	5 1 2	latjlej2	$$⊢\left(K\in \mathrm{Lat}\wedge \left(U\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\right)\to \left(U\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\right)$$
89	7 23 25 16 88	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(U\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\right)$$
90	37 89	mpd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
91	90	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
92	87 91	eqbrtrrd	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
93	5 2 3	hlatjcl	$$⊢\left(K\in \mathrm{HL}\wedge S\in A\wedge U\in A\right)\to S\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
94	6 17 21 93	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
95	5 1 2	latlej2	$$⊢\left(K\in \mathrm{Lat}\wedge S\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge T\in {\mathrm{Base}}_K\right)\to T\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }T\right)$$
96	7 94 59 95	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }T\right)$$
97	2 3	hlatj32	$$⊢\left(K\in \mathrm{HL}\wedge \left(S\in A\wedge T\in A\wedge U\in A\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }T$$
98	6 17 18 21 97	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=\left(S\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\vee }T$$
99	96 98	breqtrrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
100	5 1 7 59 25 30 99 32	lattrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\underset{\dot{}}{\le }W$$
101	5 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge T\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }W\right)$$
102	7 16 59 30 101	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge T\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }W\right)$$
103	31 100 102	mpbi2and	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }W$$
104	103	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }W$$
105	6	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to K\in \mathrm{HL}$$
106	44	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
107	12 18	jca	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(R\in A\wedge T\in A\right)$$
108	107	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(R\in A\wedge T\in A\right)$$
109	48	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to P\ne Q$$
110	50	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
111		simpr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
112	1 2 3 4	lvoli2	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge T\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\in V$$
113	106 108 109 110 111 112	syl113anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\in V$$
114	28	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\in V$$
115	1 4	lvolcmp	$$⊢\left(K\in \mathrm{HL}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\in V\wedge W\in V\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }W\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T=W\right)$$
116	105 113 114 115	syl3anc	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }W\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T=W\right)$$
117	104 116	mpbid	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T=W$$
118	5 1 2	latjlej2	$$⊢\left(K\in \mathrm{Lat}\wedge \left(T\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\right)\to \left(T\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\right)$$
119	7 59 25 16 118	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(T\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\right)$$
120	99 119	mpd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
121	120	ad2antrr	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
122	117 121	eqbrtrrd	$$⊢\left(\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\wedge \neg T\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
123	92 122	pm2.61dan	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
124	5 2 3	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$$
125	6 18 21 124	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K$$
126	5 1 2	latlej1	$$⊢\left(K\in \mathrm{Lat}\wedge S\in {\mathrm{Base}}_K\wedge T\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
127	7 57 125 126	syl3anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)\right)$$
128	5 2	latjass	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\in {\mathrm{Base}}_K\wedge T\in {\mathrm{Base}}_K\wedge U\in {\mathrm{Base}}_K\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)$$
129	7 57 59 23 128	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U=S\underset{\dot{}}{\vee }\left(T\underset{\dot{}}{\vee }U\right)$$
130	127 129	breqtrrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)$$
131	5 1 7 57 25 30 130 32	lattrd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to S\underset{\dot{}}{\le }W$$
132	5 1 2	latjle12	$$⊢\left(K\in \mathrm{Lat}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\wedge S\in {\mathrm{Base}}_K\wedge W\in {\mathrm{Base}}_K\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }W\right)$$
133	7 16 57 30 132	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge S\underset{\dot{}}{\le }W\right)\leftrightarrow \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }W\right)$$
134	31 131 133	mpbi2and	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }W$$
135	134	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }W$$
136	6	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to K\in \mathrm{HL}$$
137	44	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)$$
138	12 17	jca	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(R\in A\wedge S\in A\right)$$
139	138	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(R\in A\wedge S\in A\right)$$
140	48	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to P\ne Q$$
141	50	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)$$
142		simpr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)$$
143	1 2 3 4	lvoli2	$$⊢\left(\left(K\in \mathrm{HL}\wedge P\in A\wedge Q\in A\right)\wedge \left(R\in A\wedge S\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V$$
144	137 139 140 141 142 143	syl113anc	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V$$
145	28	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\in V$$
146	1 4	lvolcmp	$$⊢\left(K\in \mathrm{HL}\wedge \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\in V\wedge W\in V\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }W\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=W\right)$$
147	136 144 145 146	syl3anc	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }W\leftrightarrow \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=W\right)$$
148	135 147	mpbid	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S=W$$
149	5 1 2	latjlej2	$$⊢\left(K\in \mathrm{Lat}\wedge \left(S\in {\mathrm{Base}}_K\wedge \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\in {\mathrm{Base}}_K\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\in {\mathrm{Base}}_K\right)\right)\to \left(S\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\right)$$
150	7 57 25 16 149	syl13anc	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(S\underset{\dot{}}{\le }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\right)$$
151	130 150	mpd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
152	151	adantr	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }S\right)\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
153	148 152	eqbrtrrd	$$⊢\left(\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\wedge \neg S\underset{\dot{}}{\le }\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\right)\to W\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
154	123 153	pm2.61dan	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to W\underset{\dot{}}{\le }\left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)$$
155	5 1 7 27 30 35 154	latasymd	$$⊢\left(\left(\left(K\in \mathrm{HL}\wedge W\in V\right)\wedge \left(P\in A\wedge Q\in A\wedge R\in A\right)\wedge \left(P\ne Q\wedge \neg R\underset{\dot{}}{\le }\left(P\underset{\dot{}}{\vee }Q\right)\right)\right)\wedge \left(\left(S\in A\wedge T\in A\wedge U\in A\right)\wedge \left(S\ne T\wedge \neg U\underset{\dot{}}{\le }\left(S\underset{\dot{}}{\vee }T\right)\right)\right)\wedge \left(\left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\le }W\wedge \left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\underset{\dot{}}{\le }W\wedge \left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\ne \left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)\right)\to \left(\left(P\underset{\dot{}}{\vee }Q\right)\underset{\dot{}}{\vee }R\right)\underset{\dot{}}{\vee }\left(\left(S\underset{\dot{}}{\vee }T\right)\underset{\dot{}}{\vee }U\right)=W$$