---

Step * of Lemma geo-line-eq_inversion

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

1
1. g : EuclideanPlane
2. l : Line
3. m : Line
4. l ≡ m
5. p : Point
6. Colinear(p;fst(m);fst(snd(m))) ∧ p # fst(l)fst(snd(l))
⊢ False

---

Latex:

---

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


By

---

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

---

Home Index