---

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


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)
16. p # bc
⊢ False
BY
{ ((Thin (14) THEN Thin (13)) THEN (Assert a ≠ b BY ((D 5 THEN D 6) THEN All Reduce 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;a;b)
14. p # bc
15. a ≠ b
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  a  :  Point
3.  b  :  Point
4.  c  :  Point
5.  l  :  Line
6.  a  \mequiv{}  fst(l)
7.  b  \mequiv{}  fst(snd(l))
8.  m  :  Line
9.  b  \mequiv{}  fst(m)
10.  c  \mequiv{}  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)
16.  p  \#  bc
\mvdash{}  False


By

---

Latex:
((Thin  (14)  THEN  Thin  (13))  THEN  (Assert  a  \mneq{}  b  BY  ((D  5  THEN  D  6)  THEN  All  Reduce  THEN  Auto)))

---

Home Index