---

Step * of Lemma geo-colinear-line-eq2

∀e:EuclideanPlane. ∀l1,l2:Line.
  (Colinear(fst(l1);fst(l2);fst(snd(l2))) ⇒ Colinear(fst(snd(l1));fst(l2);fst(snd(l2))) ⇒ l1 ≡ l2)
BY
{ ((((Auto THEN Unfold `geo-line-eq` 0) THEN (D 0 THENA Auto)) THEN Unfold `geo-line-sep` -1)
   THEN (InstLemma `geo-sep-or` [⌜e⌝;⌜fst(l2)⌝;fst(snd(l2));⌜fst(l1)⌝]⋅ THENA Auto)
   THEN D -1) }

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. (Colinear(p;fst(l1);fst(snd(l1))) ∧ p # fst(l2)fst(snd(l2)))
7. fst(l2) ≠ fst(l1)
⊢ False

2
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

---

Latex:

---

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}l1,l2:Line.
    (Colinear(fst(l1);fst(l2);fst(snd(l2)))  {}\mRightarrow{}  Colinear(fst(snd(l1));fst(l2);fst(snd(l2)))  {}\mRightarrow{}  l1  \mequiv{}  l2)


By

---

Latex:
((((Auto  THEN  Unfold  `geo-line-eq`  0)  THEN  (D  0  THENA  Auto))  THEN  Unfold  `geo-line-sep`  -1)
  THEN  (InstLemma  `geo-sep-or`  [\mkleeneopen{}e\mkleeneclose{};\mkleeneopen{}fst(l2)\mkleeneclose{};fst(snd(l2));\mkleeneopen{}fst(l1)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1)

---

Home Index