---

Step * of Lemma geo-sep-iff-or-lt

∀e:BasicGeometry. ∀x,y:{p:Point| O_X_p} .  (x ≠ y ⇐⇒ x < y ∨ y < x)
BY
{ Auto }

1
1. e : BasicGeometry
2. x : {p:Point| O_X_p} 
3. y : {p:Point| O_X_p} 
4. x ≠ y
⊢ x < y ∨ y < x

2
1. e : BasicGeometry
2. x : {p:Point| O_X_p} 
3. y : {p:Point| O_X_p} 
4. x < y ∨ y < x
⊢ x ≠ y

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}x,y:\{p:Point|  O\_X\_p\}  .    (x  \mneq{}  y  \mLeftarrow{}{}\mRightarrow{}  x  <  y  \mvee{}  y  <  x)


By

---

Latex:
Auto

---

Home Index