Step
*
1
of Lemma
hp-right-angles-out
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. p1 : Point
5. p2 : Point
6. Rbap1
7. Rbap2
8. p1 # ab
9. p1 leftof ab
⇒ p2 leftof ab
10. p1 leftof ab
⇐ p2 leftof ab
11. p1 leftof ba
⇒ p2 leftof ba
12. p1 leftof ba
⇐ p2 leftof ba
⊢ a ≠ p2
BY
{ (D 8 THEN Auto) }
Latex:
Latex:
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. p1 : Point
5. p2 : Point
6. Rbap1
7. Rbap2
8. p1 \# ab
9. p1 leftof ab {}\mRightarrow{} p2 leftof ab
10. p1 leftof ab \mLeftarrow{}{} p2 leftof ab
11. p1 leftof ba {}\mRightarrow{} p2 leftof ba
12. p1 leftof ba \mLeftarrow{}{} p2 leftof ba
\mvdash{} a \mneq{} p2
By
Latex:
(D 8 THEN Auto)
Home
Index