---

Step * of Lemma geo-lt_transitivity2

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

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

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  4  (ParallelOp  -2))

---

Home Index