---

Step * of Lemma geo-line-sep-symmetry

No Annotations
∀g:EuclideanParPlane. ∀l,m:Line.  (((l # m) ∧ (∀L,M,N:Line.  (L \/ M ⇒ (L \/ N ∨ M \/ N)))) ⇒ (m # l))
BY
{ (Auto
   THEN skip{(GetLinePoints 3
              THEN GetLinePoints 2
              THEN All (RepUR ``geo-line-sep``)
              THEN ExRepD
              THEN (InstLemma `Euclid-drop-perp-00` [⌜g⌝;⌜x⌝;⌜y⌝;⌜p⌝]⋅ THENA Auto)
              THEN ExRepD
              THEN skip{(RenameVar `q' (-3) THEN D -1)})}
   ) }

1
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)

---

Latex:

---

Latex:
No  Annotations
\mforall{}g:EuclideanParPlane.  \mforall{}l,m:Line.
    (((l  \#  m)  \mwedge{}  (\mforall{}L,M,N:Line.    (L  \mbackslash{}/  M  {}\mRightarrow{}  (L  \mbackslash{}/  N  \mvee{}  M  \mbackslash{}/  N))))  {}\mRightarrow{}  (m  \#  l))


By

---

Latex:
(Auto
  THEN  skip\{(GetLinePoints  3
                        THEN  GetLinePoints  2
                        THEN  All  (RepUR  ``geo-line-sep``)
                        THEN  ExRepD
                        THEN  (InstLemma  `Euclid-drop-perp-00`  [\mkleeneopen{}g\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{}]\mcdot{}  THENA  Auto)
                        THEN  ExRepD
                        THEN  skip\{(RenameVar  `q'  (-3)  THEN  D  -1)\})\}
  )

---

Home Index