---

Step * 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)
⊢ False
BY
{ (Assert p # bc BY
         ((((Assert fst(m) ≡ b BY Auto) THEN (Assert fst(snd(m)) ≡ c BY Auto))
           THEN (RWO "16" 14 THENA Auto)
           THEN (RWO "17" 14 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)
16. p # bc
⊢ 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)
\mvdash{}  False


By

---

Latex:
(Assert  p  \#  bc  BY
              ((((Assert  fst(m)  \mequiv{}  b  BY  Auto)  THEN  (Assert  fst(snd(m))  \mequiv{}  c  BY  Auto))
                  THEN  (RWO  "16"  14  THENA  Auto)
                  THEN  (RWO  "17"  14  THENA  Auto))
                THEN  Auto
                ))

---

Home Index