---

Step * 1 of Lemma geo-line-eq_transitivity


1. g : EuclideanPlane
2. l : Line
3. m : Line
4. n : Line
5. l ≡ m
6. m ≡ n
7. geo-line-sep(g;l;n)
⊢ False
BY
{ ((Unfold `geo-line-sep` -1
    THEN (InstLemma `geo-line-eq-to-col` [⌜g⌝;⌜l⌝;⌜m⌝]⋅ THENA Auto)
    THEN (InstLemma `geo-line-eq-to-col` [⌜g⌝;⌜m⌝;⌜n⌝]⋅ THENA Auto))
   THEN ExRepD
   ) }

1
1. g : EuclideanPlane
2. l : Line
3. m : Line
4. n : Line
5. l ≡ m
6. m ≡ n
7. p : Point
8. Colinear(p;fst(l);fst(snd(l)))
9. p # fst(n)fst(snd(n))
10. Colinear(fst(l);fst(snd(l));fst(m))
11. Colinear(fst(l);fst(snd(l));fst(snd(m)))
12. Colinear(fst(m);fst(snd(m));fst(n))
13. Colinear(fst(m);fst(snd(m));fst(snd(n)))
⊢ False

---

Latex:

---

Latex:

1.  g  :  EuclideanPlane
2.  l  :  Line
3.  m  :  Line
4.  n  :  Line
5.  l  \mequiv{}  m
6.  m  \mequiv{}  n
7.  geo-line-sep(g;l;n)
\mvdash{}  False


By

---

Latex:
((Unfold  `geo-line-sep`  -1
    THEN  (InstLemma  `geo-line-eq-to-col`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  (InstLemma  `geo-line-eq-to-col`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  ExRepD
  )

---

Home Index