Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Projective geometries based on Hilbert lattices
4atlem12
Next ⟩
4at
Metamath Proof Explorer
Ascii
Unicode
Theorem
4atlem12
Description:
Lemma for
4at
. Combine all four possible cases.
(Contributed by
NM
, 11-Jul-2012)
Ref
Expression
Hypotheses
4at.l
⊢
≤
˙
=
≤
K
4at.j
⊢
∨
˙
=
join
K
4at.a
⊢
A
=
Atoms
K
Assertion
4atlem12
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
Proof
Step
Hyp
Ref
Expression
1
4at.l
⊢
≤
˙
=
≤
K
2
4at.j
⊢
∨
˙
=
join
K
3
4at.a
⊢
A
=
Atoms
K
4
simpl11
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
5
4
hllatd
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
Lat
6
simpl12
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∈
A
7
eqid
⊢
Base
K
=
Base
K
8
7
3
atbase
⊢
P
∈
A
→
P
∈
Base
K
9
6
8
syl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∈
Base
K
10
simpl13
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
Q
∈
A
11
7
3
atbase
⊢
Q
∈
A
→
Q
∈
Base
K
12
10
11
syl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
Q
∈
Base
K
13
simpl23
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
T
∈
A
14
simpl31
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
U
∈
A
15
7
2
3
hlatjcl
⊢
K
∈
HL
∧
T
∈
A
∧
U
∈
A
→
T
∨
˙
U
∈
Base
K
16
4
13
14
15
syl3anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
T
∨
˙
U
∈
Base
K
17
simpl32
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
V
∈
A
18
simpl33
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
W
∈
A
19
7
2
3
hlatjcl
⊢
K
∈
HL
∧
V
∈
A
∧
W
∈
A
→
V
∨
˙
W
∈
Base
K
20
4
17
18
19
syl3anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
V
∨
˙
W
∈
Base
K
21
7
2
latjcl
⊢
K
∈
Lat
∧
T
∨
˙
U
∈
Base
K
∧
V
∨
˙
W
∈
Base
K
→
T
∨
˙
U
∨
˙
V
∨
˙
W
∈
Base
K
22
5
16
20
21
syl3anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
T
∨
˙
U
∨
˙
V
∨
˙
W
∈
Base
K
23
7
1
2
latjle12
⊢
K
∈
Lat
∧
P
∈
Base
K
∧
Q
∈
Base
K
∧
T
∨
˙
U
∨
˙
V
∨
˙
W
∈
Base
K
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
P
∨
˙
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
24
5
9
12
22
23
syl13anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
P
∨
˙
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
25
simpl21
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
∈
A
26
7
3
atbase
⊢
R
∈
A
→
R
∈
Base
K
27
25
26
syl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
∈
Base
K
28
simpl22
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
S
∈
A
29
7
3
atbase
⊢
S
∈
A
→
S
∈
Base
K
30
28
29
syl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
S
∈
Base
K
31
7
1
2
latjle12
⊢
K
∈
Lat
∧
R
∈
Base
K
∧
S
∈
Base
K
∧
T
∨
˙
U
∨
˙
V
∨
˙
W
∈
Base
K
→
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
32
5
27
30
22
31
syl13anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
33
24
32
anbi12d
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
P
∨
˙
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
34
simpl1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
35
7
2
3
hlatjcl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
→
P
∨
˙
Q
∈
Base
K
36
34
35
syl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∨
˙
Q
∈
Base
K
37
7
2
3
hlatjcl
⊢
K
∈
HL
∧
R
∈
A
∧
S
∈
A
→
R
∨
˙
S
∈
Base
K
38
4
25
28
37
syl3anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
∨
˙
S
∈
Base
K
39
7
1
2
latjle12
⊢
K
∈
Lat
∧
P
∨
˙
Q
∈
Base
K
∧
R
∨
˙
S
∈
Base
K
∧
T
∨
˙
U
∨
˙
V
∨
˙
W
∈
Base
K
→
P
∨
˙
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
P
∨
˙
Q
∨
˙
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
40
5
36
38
22
39
syl13anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∨
˙
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
P
∨
˙
Q
∨
˙
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
41
33
40
bitrd
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
↔
P
∨
˙
Q
∨
˙
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
42
simp1l
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
43
simp1r
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
44
simp2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
45
simp3
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
46
1
2
3
4atlem12b
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
47
42
43
44
45
46
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
48
47
3exp
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
49
7
2
latj4rot
⊢
K
∈
Lat
∧
Q
∈
Base
K
∧
R
∈
Base
K
∧
S
∈
Base
K
∧
P
∈
Base
K
→
Q
∨
˙
R
∨
˙
S
∨
˙
P
=
P
∨
˙
Q
∨
˙
R
∨
˙
S
50
5
12
27
30
9
49
syl122anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
Q
∨
˙
R
∨
˙
S
∨
˙
P
=
P
∨
˙
Q
∨
˙
R
∨
˙
S
51
50
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
∨
˙
R
∨
˙
S
∨
˙
P
=
P
∨
˙
Q
∨
˙
R
∨
˙
S
52
4
10
25
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
Q
∈
A
∧
R
∈
A
53
28
6
13
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
S
∈
A
∧
P
∈
A
∧
T
∈
A
54
simpl3
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
U
∈
A
∧
V
∈
A
∧
W
∈
A
55
52
53
54
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
P
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
56
55
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
K
∈
HL
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
P
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
57
simpr
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
58
1
2
3
4noncolr3
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
Q
≠
R
∧
¬
S
≤
˙
Q
∨
˙
R
∧
¬
P
≤
˙
Q
∨
˙
R
∨
˙
S
59
34
25
28
57
58
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
Q
≠
R
∧
¬
S
≤
˙
Q
∨
˙
R
∧
¬
P
≤
˙
Q
∨
˙
R
∨
˙
S
60
59
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
≠
R
∧
¬
S
≤
˙
Q
∨
˙
R
∧
¬
P
≤
˙
Q
∨
˙
R
∨
˙
S
61
simp2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
62
simprlr
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
63
simprrl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
64
62
63
jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
65
simprrr
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
66
simprll
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
67
64
65
66
jca32
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
68
67
3adant2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
69
1
2
3
4atlem12b
⊢
K
∈
HL
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
P
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
Q
≠
R
∧
¬
S
≤
˙
Q
∨
˙
R
∧
¬
P
≤
˙
Q
∨
˙
R
∨
˙
S
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
∨
˙
R
∨
˙
S
∨
˙
P
=
T
∨
˙
U
∨
˙
V
∨
˙
W
70
56
60
61
68
69
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
Q
∨
˙
R
∨
˙
S
∨
˙
P
=
T
∨
˙
U
∨
˙
V
∨
˙
W
71
51
70
eqtr3d
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
72
71
3exp
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
73
48
72
jaod
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
74
7
2
latjcom
⊢
K
∈
Lat
∧
P
∨
˙
Q
∈
Base
K
∧
R
∨
˙
S
∈
Base
K
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
R
∨
˙
S
∨
˙
P
∨
˙
Q
75
5
36
38
74
syl3anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
R
∨
˙
S
∨
˙
P
∨
˙
Q
76
75
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
R
∨
˙
S
∨
˙
P
∨
˙
Q
77
4
25
28
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
R
∈
A
∧
S
∈
A
78
6
10
13
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∈
A
∧
Q
∈
A
∧
T
∈
A
79
77
78
54
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
R
∈
A
∧
S
∈
A
∧
P
∈
A
∧
Q
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
80
79
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
K
∈
HL
∧
R
∈
A
∧
S
∈
A
∧
P
∈
A
∧
Q
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
81
1
2
3
4noncolr2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
≠
S
∧
¬
P
≤
˙
R
∨
˙
S
∧
¬
Q
≤
˙
R
∨
˙
S
∨
˙
P
82
34
25
28
57
81
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
≠
S
∧
¬
P
≤
˙
R
∨
˙
S
∧
¬
Q
≤
˙
R
∨
˙
S
∨
˙
P
83
82
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
≠
S
∧
¬
P
≤
˙
R
∨
˙
S
∧
¬
Q
≤
˙
R
∨
˙
S
∨
˙
P
84
simp2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
85
simprr
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
86
simprl
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
87
85
86
jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
88
87
3adant2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
89
1
2
3
4atlem12b
⊢
K
∈
HL
∧
R
∈
A
∧
S
∈
A
∧
P
∈
A
∧
Q
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
R
≠
S
∧
¬
P
≤
˙
R
∨
˙
S
∧
¬
Q
≤
˙
R
∨
˙
S
∨
˙
P
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
∨
˙
S
∨
˙
P
∨
˙
Q
=
T
∨
˙
U
∨
˙
V
∨
˙
W
90
80
83
84
88
89
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
R
∨
˙
S
∨
˙
P
∨
˙
Q
=
T
∨
˙
U
∨
˙
V
∨
˙
W
91
76
90
eqtrd
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
92
91
3exp
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
93
7
2
latj4rot
⊢
K
∈
Lat
∧
P
∈
Base
K
∧
Q
∈
Base
K
∧
R
∈
Base
K
∧
S
∈
Base
K
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
S
∨
˙
P
∨
˙
Q
∨
˙
R
94
5
9
12
27
30
93
syl122anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
S
∨
˙
P
∨
˙
Q
∨
˙
R
95
94
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
S
∨
˙
P
∨
˙
Q
∨
˙
R
96
4
28
6
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
S
∈
A
∧
P
∈
A
97
10
25
13
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
Q
∈
A
∧
R
∈
A
∧
T
∈
A
98
96
97
54
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
K
∈
HL
∧
S
∈
A
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
99
98
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
K
∈
HL
∧
S
∈
A
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
100
1
2
3
4noncolr1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
S
≠
P
∧
¬
Q
≤
˙
S
∨
˙
P
∧
¬
R
≤
˙
S
∨
˙
P
∨
˙
Q
101
34
25
28
57
100
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
S
≠
P
∧
¬
Q
≤
˙
S
∨
˙
P
∧
¬
R
≤
˙
S
∨
˙
P
∨
˙
Q
102
101
3ad2ant1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
≠
P
∧
¬
Q
≤
˙
S
∨
˙
P
∧
¬
R
≤
˙
S
∨
˙
P
∨
˙
Q
103
simp2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
104
65
66
jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
105
104
62
63
jca32
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
106
105
3adant2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
107
1
2
3
4atlem12b
⊢
K
∈
HL
∧
S
∈
A
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
S
≠
P
∧
¬
Q
≤
˙
S
∨
˙
P
∧
¬
R
≤
˙
S
∨
˙
P
∨
˙
Q
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
∨
˙
P
∨
˙
Q
∨
˙
R
=
T
∨
˙
U
∨
˙
V
∨
˙
W
108
99
102
103
106
107
syl121anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
S
∨
˙
P
∨
˙
Q
∨
˙
R
=
T
∨
˙
U
∨
˙
V
∨
˙
W
109
95
108
eqtrd
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
∧
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
∧
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
110
109
3exp
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
111
92
110
jaod
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
112
25
28
14
3jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
R
∈
A
∧
S
∈
A
∧
U
∈
A
113
17
18
jca
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
V
∈
A
∧
W
∈
A
114
1
2
3
4atlem3
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
115
34
112
113
57
114
syl31anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
¬
P
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
Q
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
R
≤
˙
U
∨
˙
V
∨
˙
W
∨
¬
S
≤
˙
U
∨
˙
V
∨
˙
W
116
73
111
115
mpjaod
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
Q
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
R
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
∧
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W
117
41
116
sylbird
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
S
∈
A
∧
T
∈
A
∧
U
∈
A
∧
V
∈
A
∧
W
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
∧
¬
S
≤
˙
P
∨
˙
Q
∨
˙
R
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
≤
˙
T
∨
˙
U
∨
˙
V
∨
˙
W
→
P
∨
˙
Q
∨
˙
R
∨
˙
S
=
T
∨
˙
U
∨
˙
V
∨
˙
W