---

Step * of Lemma geo-lt_transitivity

∀e:BasicGeometry. ∀p,q,r:Length.  (p ≤ q ⇒ q < r ⇒ p < r)
BY
{ (Auto THEN RepeatFor 4 (ParallelLast)) }

1
1. e : BasicGeometry
2. p : Length
3. q : Length
4. r : Length
5. p ≤ q
6. a : Point
7. b : Point
8. a ≠ b
9. q + |ab| ≤ r
⊢ p + |ab| ≤ r

---

Latex:

---

Latex:
\mforall{}e:BasicGeometry.  \mforall{}p,q,r:Length.    (p  \mleq{}  q  {}\mRightarrow{}  q  <  r  {}\mRightarrow{}  p  <  r)


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelLast))

---

Home Index