Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β πΎ β HL) |
2 | | simp11r 1286 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β π β π») |
3 | | simp2l 1200 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β π β πΈ) |
4 | | simp13 1206 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β πΊ β π) |
5 | | simp2r 1201 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (π β π΄ β§ Β¬ π β€ π)) |
6 | | cdlemi.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
7 | | cdlemi.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
8 | | cdlemi.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
9 | | cdlemi.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
10 | | cdlemi.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
11 | | cdlemi.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
12 | | cdlemi.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
13 | | cdlemi.r |
. . . . . 6
β’ π
= ((trLβπΎ)βπ) |
14 | | cdlemi.e |
. . . . . 6
β’ πΈ = ((TEndoβπΎ)βπ) |
15 | 6, 7, 8, 9, 10, 11, 12, 13, 14 | cdlemi1 39284 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (π β¨ (π
βπΊ))) |
16 | 1, 2, 3, 4, 5, 15 | syl221anc 1382 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) β€ (π β¨ (π
βπΊ))) |
17 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β πΉ β π) |
18 | 6, 7, 8, 9, 10, 11, 12, 13, 14 | cdlemi2 39285 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) |
19 | 1, 2, 3, 17, 4, 5,
18 | syl231anc 1391 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) β€ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) |
20 | 1 | hllatd 37829 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β πΎ β Lat) |
21 | | simp11 1204 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (πΎ β HL β§ π β π»)) |
22 | 11, 12, 14 | tendocl 39233 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΊ β π) β (πβπΊ) β π) |
23 | 21, 3, 4, 22 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (πβπΊ) β π) |
24 | | simp2rl 1243 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β π β π΄) |
25 | 6, 10 | atbase 37754 |
. . . . . . 7
β’ (π β π΄ β π β π΅) |
26 | 24, 25 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β π β π΅) |
27 | 6, 11, 12 | ltrncl 38591 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πβπΊ) β π β§ π β π΅) β ((πβπΊ)βπ) β π΅) |
28 | 21, 23, 26, 27 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) β π΅) |
29 | 6, 11, 12, 13 | trlcl 38630 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β π΅) |
30 | 21, 4, 29 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (π
βπΊ) β π΅) |
31 | 6, 8 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ (π
βπΊ) β π΅) β (π β¨ (π
βπΊ)) β π΅) |
32 | 20, 26, 30, 31 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (π β¨ (π
βπΊ)) β π΅) |
33 | 11, 12, 14 | tendocl 39233 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) |
34 | 21, 3, 17, 33 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (πβπΉ) β π) |
35 | 6, 11, 12 | ltrncl 38591 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π β§ π β π΅) β ((πβπΉ)βπ) β π΅) |
36 | 21, 34, 26, 35 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΉ)βπ) β π΅) |
37 | 11, 12 | ltrncnv 38612 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) |
38 | 21, 17, 37 | syl2anc 585 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β β‘πΉ β π) |
39 | 11, 12 | ltrnco 39185 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ β‘πΉ β π) β (πΊ β β‘πΉ) β π) |
40 | 21, 4, 38, 39 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (πΊ β β‘πΉ) β π) |
41 | 6, 11, 12, 13 | trlcl 38630 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΊ β β‘πΉ) β π) β (π
β(πΊ β β‘πΉ)) β π΅) |
42 | 21, 40, 41 | syl2anc 585 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (π
β(πΊ β β‘πΉ)) β π΅) |
43 | 6, 8 | latjcl 18329 |
. . . . . 6
β’ ((πΎ β Lat β§ ((πβπΉ)βπ) β π΅ β§ (π
β(πΊ β β‘πΉ)) β π΅) β (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ))) β π΅) |
44 | 20, 36, 42, 43 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ))) β π΅) |
45 | 6, 7, 9 | latlem12 18356 |
. . . . 5
β’ ((πΎ β Lat β§ (((πβπΊ)βπ) β π΅ β§ (π β¨ (π
βπΊ)) β π΅ β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ))) β π΅)) β ((((πβπΊ)βπ) β€ (π β¨ (π
βπΊ)) β§ ((πβπΊ)βπ) β€ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β ((πβπΊ)βπ) β€ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))))) |
46 | 20, 28, 32, 44, 45 | syl13anc 1373 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((((πβπΊ)βπ) β€ (π β¨ (π
βπΊ)) β§ ((πβπΊ)βπ) β€ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β ((πβπΊ)βπ) β€ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))))) |
47 | 16, 19, 46 | mpbi2and 711 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) β€ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ))))) |
48 | | hlatl 37825 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
49 | 1, 48 | syl 17 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β πΎ β AtLat) |
50 | 7, 10, 11, 12 | ltrnat 38606 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πβπΊ) β π β§ π β π΄) β ((πβπΊ)βπ) β π΄) |
51 | 21, 23, 24, 50 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) β π΄) |
52 | 7, 10, 11, 12 | ltrnel 38605 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πβπΉ) β π β§ (π β π΄ β§ Β¬ π β€ π)) β (((πβπΉ)βπ) β π΄ β§ Β¬ ((πβπΉ)βπ) β€ π)) |
53 | 21, 34, 5, 52 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (((πβπΉ)βπ) β π΄ β§ Β¬ ((πβπΉ)βπ) β€ π)) |
54 | 6, 7, 8, 9, 10, 11, 12, 13, 14 | cdlemi1 39284 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΉ)βπ) β€ (π β¨ (π
βπΉ))) |
55 | 1, 2, 3, 17, 5, 54 | syl221anc 1382 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΉ)βπ) β€ (π β¨ (π
βπΉ))) |
56 | 5, 53, 55 | 3jca 1129 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((π β π΄ β§ Β¬ π β€ π) β§ (((πβπΉ)βπ) β π΄ β§ Β¬ ((πβπΉ)βπ) β€ π) β§ ((πβπΉ)βπ) β€ (π β¨ (π
βπΉ)))) |
57 | | eqid 2737 |
. . . . . . 7
β’ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) = ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) |
58 | 6, 7, 8, 9, 10, 11, 12, 13, 57 | cdlemh 39283 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (((πβπΉ)βπ) β π΄ β§ Β¬ ((πβπΉ)βπ) β€ π) β§ ((πβπΉ)βπ) β€ (π β¨ (π
βπΉ))) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β π΄ β§ Β¬ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β€ π)) |
59 | 58 | simpld 496 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (((πβπΉ)βπ) β π΄ β§ Β¬ ((πβπΉ)βπ) β€ π) β§ ((πβπΉ)βπ) β€ (π β¨ (π
βπΉ))) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β π΄) |
60 | 56, 59 | syld3an2 1412 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β π΄) |
61 | 7, 10 | atcmp 37776 |
. . . 4
β’ ((πΎ β AtLat β§ ((πβπΊ)βπ) β π΄ β§ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β π΄) β (((πβπΊ)βπ) β€ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))))) |
62 | 49, 51, 60, 61 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β (((πβπΊ)βπ) β€ ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))))) |
63 | 47, 62 | mpbid 231 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) = ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ))))) |
64 | | cdlemi.s |
. 2
β’ π = ((π β¨ (π
βπΊ)) β§ (((πβπΉ)βπ) β¨ (π
β(πΊ β β‘πΉ)))) |
65 | 63, 64 | eqtr4di 2795 |
1
β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π
βπΉ) β (π
βπΊ))) β ((πβπΊ)βπ) = π) |