---

Step * 1 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;a;b)
14. p # bc
15. a ≠ b
⊢ False
BY
{ ((Assert p # ba BY Auto) THEN EAuto 2) }

---

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;a;b)
14.  p  \#  bc
15.  a  \mneq{}  b
\mvdash{}  False


By

---

Latex:
((Assert  p  \#  ba  BY  Auto)  THEN  EAuto  2)

---

Home Index