Step
*
1
1
1
1
1
1
1
of Lemma
perp-aux2
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. r : Point
8. a # bc
9. a-p-b
10. c-q-b
11. a-r-c
12. y : Point
13. p-y-c
14. q-y-r
15. p # bc
16. q # pc
17. y # pq
18. r # qp
⊢ p # qr
BY
{ Auto }
Latex:
Latex:
1. e : HeytingGeometry
2. a : Point
3. b : Point
4. c : Point
5. p : Point
6. q : Point
7. r : Point
8. a \# bc
9. a-p-b
10. c-q-b
11. a-r-c
12. y : Point
13. p-y-c
14. q-y-r
15. p \# bc
16. q \# pc
17. y \# pq
18. r \# qp
\mvdash{} p \# qr
By
Latex:
Auto
Home
Index