---

Step * 1 1 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
7. Colinear(p;fst(l1);fst(snd(l1)))
8. p # fst(l2)fst(snd(l2))
9. fst(l2) ≠ fst(l1)
10. p # fst(l2)fst(l1)
11. Colinear(fst(l1);fst(snd(l1));fst(l2))
⊢ False
BY
{ ((Assert p # fst(snd(l1))fst(l1) BY
          (((Lemmaize [-1;-2] THEN Auto)
            THEN (InstLemma `colinear-lsep\'` [⌜e⌝;⌜fst(l2)⌝;⌜fst(l1)⌝;⌜fst(snd(l1))⌝;⌜p⌝]⋅
                  THENA (Auto THEN (D 2 THEN D 3) THEN Auto)
                  )
            )
           THEN Auto
           ))
   THEN Lemmaize [-1;7]
   THEN EAuto 2) }

---

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.  p  :  Point
7.  Colinear(p;fst(l1);fst(snd(l1)))
8.  p  \#  fst(l2)fst(snd(l2))
9.  fst(l2)  \mneq{}  fst(l1)
10.  p  \#  fst(l2)fst(l1)
11.  Colinear(fst(l1);fst(snd(l1));fst(l2))
\mvdash{}  False


By

---

Latex:
((Assert  p  \#  fst(snd(l1))fst(l1)  BY
                (((Lemmaize  [-1;-2]  THEN  Auto)
                    THEN  (InstLemma  `colinear-lsep\mbackslash{}'`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}fst(l2)\mkleeneclose{};\mkleeneopen{}fst(l1)\mkleeneclose{};\mkleeneopen{}fst(snd(l1))\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}
                                THENA  (Auto  THEN  (D  2  THEN  D  3)  THEN  Auto)
                                )
                    )
                  THEN  Auto
                  ))
  THEN  Lemmaize  [-1;7]
  THEN  EAuto  2)

---

Home Index