---

Step * 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
⊢ p ≡ q
BY
{ (Assert O_p_q ∧ O_q_p ∧ O ≠ p ∧ O ≠ q BY
         Auto) }

1
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

---

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
\mvdash{}  p  \mequiv{}  q


By

---

Latex:
(Assert  O\_p\_q  \mwedge{}  O\_q\_p  \mwedge{}  O  \mneq{}  p  \mwedge{}  O  \mneq{}  q  BY
              Auto)

---

Home Index