---

Step * 1 of Lemma geo-line-sep-symmetry


1. g : EuclideanParPlane
2. l : Line
3. m : Line
4. (l # m)
5. ∀L,M,N:Line.  (L \/ M ⇒ (L \/ N ∨ M \/ N))
⊢ (m # l)
BY
{ (Unfold `geo-line-sep` 4
   THEN ExRepD
   THEN (InstLemma `geo-line-from-points` [⌜g⌝;⌜p⌝;⌜fst(m)⌝]⋅ THENA Auto)
   THEN (InstLemma `geo-line-from-points` [⌜g⌝;⌜p⌝;⌜fst(snd(m))⌝]⋅ THENA Auto)) }

1
1. g : EuclideanParPlane
2. l : Line
3. m : Line
4. p : Point
5. Colinear(p;fst(l);fst(snd(l)))
6. p # fst(m)fst(snd(m))
7. ∀L,M,N:Line.  (L \/ M ⇒ (L \/ N ∨ M \/ N))
8. ∃l:Line. (p ≡ fst(l) ∧ fst(m) ≡ fst(snd(l)))
9. ∃l:Line. (p ≡ fst(l) ∧ fst(snd(m)) ≡ fst(snd(l)))
⊢ (m # l)

---

Latex:

---

Latex:

1.  g  :  EuclideanParPlane
2.  l  :  Line
3.  m  :  Line
4.  (l  \#  m)
5.  \mforall{}L,M,N:Line.    (L  \mbackslash{}/  M  {}\mRightarrow{}  (L  \mbackslash{}/  N  \mvee{}  M  \mbackslash{}/  N))
\mvdash{}  (m  \#  l)


By

---

Latex:
(Unfold  `geo-line-sep`  4
  THEN  ExRepD
  THEN  (InstLemma  `geo-line-from-points`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}fst(m)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `geo-line-from-points`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}fst(snd(m))\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index