---

Step * of Lemma hp-right-angles-out

∀e:EuclideanPlane. ∀a,b,p1,p2:Point.
  (((Rbap1 ∧ Rbap2) ∧ p1 # ab ∧ (p1 leftof ab ⇐⇒ p2 leftof ab) ∧ (p1 leftof ba ⇐⇒ p2 leftof ba)) ⇒ out(a p1p2))
BY
{ ((Auto THEN D 0 THEN GenRepD) THEN Auto) }

1
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

2
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_p1_p2) ∧ (¬a_p2_p1))

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,p1,p2:Point.
    (((Rbap1  \mwedge{}  Rbap2)  \mwedge{}  p1  \#  ab  \mwedge{}  (p1  leftof  ab  \mLeftarrow{}{}\mRightarrow{}  p2  leftof  ab)  \mwedge{}  (p1  leftof  ba  \mLeftarrow{}{}\mRightarrow{}  p2  leftof  ba))
    {}\mRightarrow{}  out(a  p1p2))


By

---

Latex:
((Auto  THEN  D  0  THEN  GenRepD)  THEN  Auto)

---

Home Index