---

Step * of Lemma geo-le-iff-between-points

∀g:EuclideanPlane. ∀p,q:{p:Point| O_X_p} .  (p ≤ q ⇐⇒ X_p_q)
BY
{ Auto }

1
1. g : EuclideanPlane
2. p : {p:Point| O_X_p} 
3. q : {p:Point| O_X_p} 
4. p ≤ q
⊢ X_p_q

2
1. g : EuclideanPlane
2. p : {p:Point| O_X_p} 
3. q : {p:Point| O_X_p} 
4. X_p_q
⊢ p ≤ q

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}p,q:\{p:Point|  O\_X\_p\}  .    (p  \mleq{}  q  \mLeftarrow{}{}\mRightarrow{}  X\_p\_q)


By

---

Latex:
Auto

---

Home Index