---

Step * of Lemma geo-lt-add1-iff

∀e:BasicGeometry. ∀p,q,r:{a:Point| O_X_a} .  (X ≠ p ⇒ X ≠ q ⇒ X ≠ r ⇒ (p < q ⇐⇒ p + r < q + r))
BY
{ Auto }

1
1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a} 
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. p < q
⊢ p + r < q + r

2
1. e : BasicGeometry
2. p : {a:Point| O_X_a} 
3. q : {a:Point| O_X_a} 
4. r : {a:Point| O_X_a} 
5. X ≠ p
6. X ≠ q
7. X ≠ r
8. p + r < q + r
⊢ p < q

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q,r:\{a:Point|  O\_X\_a\}  .    (X  \mneq{}  p  {}\mRightarrow{}  X  \mneq{}  q  {}\mRightarrow{}  X  \mneq{}  r  {}\mRightarrow{}  (p  <  q  \mLeftarrow{}{}\mRightarrow{}  p  +  r  <  q  +  r))


By

---

Latex:
Auto

---

Home Index