---

Step * 2 of Lemma geo-colinear-line-eq2


1. e : EuclideanPlane
2. l1 : Line
3. l2 : Line
4. Colinear(fst(l1);fst(l2);fst(snd(l2)))
5. Colinear(fst(snd(l1));fst(l2);fst(snd(l2)))
6. ∃p:Point. (Colinear(p;fst(l1);fst(snd(l1))) ∧ p # fst(l2)fst(snd(l2)))
7. fst(snd(l2)) ≠ fst(l1)
⊢ False
BY
{ ((ExRepD THEN (Assert p # fst(snd(l2))fst(l1) BY Auto))
   THEN (Assert Colinear(fst(l1);fst(snd(l1));fst(snd(l2))) BY
               Auto)
   ) }

1
1. e : EuclideanPlane
2. l1 : Line
3. l2 : Line
4. Colinear(fst(l1);fst(l2);fst(snd(l2)))
5. Colinear(fst(snd(l1));fst(l2);fst(snd(l2)))
6. p : Point
7. Colinear(p;fst(l1);fst(snd(l1)))
8. p # fst(l2)fst(snd(l2))
9. fst(snd(l2)) ≠ fst(l1)
10. p # fst(snd(l2))fst(l1)
11. Colinear(fst(l1);fst(snd(l1));fst(snd(l2)))
⊢ False

---

Latex:

---

Latex:

1.  e  :  EuclideanPlane
2.  l1  :  Line
3.  l2  :  Line
4.  Colinear(fst(l1);fst(l2);fst(snd(l2)))
5.  Colinear(fst(snd(l1));fst(l2);fst(snd(l2)))
6.  \mexists{}p:Point.  (Colinear(p;fst(l1);fst(snd(l1)))  \mwedge{}  p  \#  fst(l2)fst(snd(l2)))
7.  fst(snd(l2))  \mneq{}  fst(l1)
\mvdash{}  False


By

---

Latex:
((ExRepD  THEN  (Assert  p  \#  fst(snd(l2))fst(l1)  BY  Auto))
  THEN  (Assert  Colinear(fst(l1);fst(snd(l1));fst(snd(l2)))  BY
                          Auto)
  )

---

Home Index