---

Step * 1 1 1 1 1 1 of Lemma geo-le_antisymmetry


1. e : BasicGeometry
2. p : Point
3. O_X_p
4. q : Point
5. O_X_q
6. X_p_q
7. X_q_p
8. O_p_q ∧ O_q_p ∧ O ≠ p ∧ O ≠ q
⊢ p ≡ q
BY
{ EAuto 1 }

---

Latex:

---

Latex:

1.  e  :  BasicGeometry
2.  p  :  Point
3.  O\_X\_p
4.  q  :  Point
5.  O\_X\_q
6.  X\_p\_q
7.  X\_q\_p
8.  O\_p\_q  \mwedge{}  O\_q\_p  \mwedge{}  O  \mneq{}  p  \mwedge{}  O  \mneq{}  q
\mvdash{}  p  \mequiv{}  q


By

---

Latex:
EAuto  1

---

Home Index