---

Step * of Lemma geo-colinear-line-eq

∀e:EuclideanPlane. ∀a,b,c:Point. ∀l:{l:Line| a ≡ fst(l) ∧ b ≡ fst(snd(l))} . ∀m:{m:Line| b ≡ fst(m) ∧ c ≡ fst(snd(m))} .
  (Colinear(a;b;c) ⇒ l ≡ m)
BY
{ (((Auto THEN Unfold `geo-line-eq` 0) THEN (D 0 THENA Auto)) THEN Unfold `geo-line-sep` -1) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. l : {l:Line| a ≡ fst(l) ∧ b ≡ fst(snd(l))} 
6. m : {m:Line| b ≡ fst(m) ∧ c ≡ fst(snd(m))} 
7. Colinear(a;b;c)
8. ∃p:Point. (Colinear(p;fst(l);fst(snd(l))) ∧ p # fst(m)fst(snd(m)))
⊢ False

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b,c:Point.  \mforall{}l:\{l:Line|  a  \mequiv{}  fst(l)  \mwedge{}  b  \mequiv{}  fst(snd(l))\}  .  \mforall{}m:\{m:Line| 
                                                                                                                                                                b  \mequiv{}  fst(m)
                                                                                                                                                                \mwedge{}  c  \mequiv{}  fst(snd(m))\}  .
    (Colinear(a;b;c)  {}\mRightarrow{}  l  \mequiv{}  m)


By

---

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

---

Home Index