---

Step * of Lemma geo-line-eq_transitivity

∀g:EuclideanPlane. ∀l,m,n:Line.  (l ≡ m ⇒ m ≡ n ⇒ l ≡ n)
BY
{ (((Auto THEN Unfold `geo-line-eq` 0) THENA Auto) THEN (D 0 THENA Auto)) }

1
1. g : EuclideanPlane
2. l : Line
3. m : Line
4. n : Line
5. l ≡ m
6. m ≡ n
7. geo-line-sep(g;l;n)
⊢ False

---

Latex:

---

Latex:
\mforall{}g:EuclideanPlane.  \mforall{}l,m,n:Line.    (l  \mequiv{}  m  {}\mRightarrow{}  m  \mequiv{}  n  {}\mRightarrow{}  l  \mequiv{}  n)


By

---

Latex:
(((Auto  THEN  Unfold  `geo-line-eq`  0)  THENA  Auto)  THEN  (D  0  THENA  Auto))

---

Home Index