---

Step * 1 of Lemma geo-colinear-line-eq


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
BY
{ (((D 5 THEN D 7) THEN ExRepD)
   THEN (Assert Colinear(p;a;b) BY
               ((((Assert fst(l) ≡ a BY Auto) THEN (Assert fst(snd(l)) ≡ b BY Auto))
                 THEN (RWO "15" 13 THENA Auto)
                 THEN (RWO "16" 13 THENA Auto))
                THEN Auto
                ))
   ) }

1
1. e : EuclideanPlane
2. a : Point
3. b : Point
4. c : Point
5. l : Line
6. a ≡ fst(l)
7. b ≡ fst(snd(l))
8. m : Line
9. b ≡ fst(m)
10. c ≡ fst(snd(m))
11. Colinear(a;b;c)
12. p : Point
13. Colinear(p;fst(l);fst(snd(l)))
14. p # fst(m)fst(snd(m))
15. Colinear(p;a;b)
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  l  :  \{l:Line|  a  \mequiv{}  fst(l)  \mwedge{}  b  \mequiv{}  fst(snd(l))\} 
6.  m  :  \{m:Line|  b  \mequiv{}  fst(m)  \mwedge{}  c  \mequiv{}  fst(snd(m))\} 
7.  Colinear(a;b;c)
8.  \mexists{}p:Point.  (Colinear(p;fst(l);fst(snd(l)))  \mwedge{}  p  \#  fst(m)fst(snd(m)))
\mvdash{}  False


By

---

Latex:
(((D  5  THEN  D  7)  THEN  ExRepD)
  THEN  (Assert  Colinear(p;a;b)  BY
                          ((((Assert  fst(l)  \mequiv{}  a  BY  Auto)  THEN  (Assert  fst(snd(l))  \mequiv{}  b  BY  Auto))
                              THEN  (RWO  "15"  13  THENA  Auto)
                              THEN  (RWO  "16"  13  THENA  Auto))
                            THEN  Auto
                            ))
  )

---

Home Index