---

Step * of Lemma P_ptsep-apartness2

∀eu:EuclideanParPlane
  ((∀l,m,n:Line.  (l \/ m ⇒ (l \/ n ∨ m \/ n)))
  ⇒ (∀p,q,r:l,m:Line//l || m. ∀P:{P:Line| p = P ∈ (l,m:Line//l || m)} . ∀Q:{Q:Line| q = Q ∈ (l,m:Line//l || m)} .
      ∀R:{R:Line| r = R ∈ (l,m:Line//l || m)} .
        (P \/ Q ⇒ (P \/ R ∨ Q \/ R))))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}eu:EuclideanParPlane
    ((\mforall{}l,m,n:Line.    (l  \mbackslash{}/  m  {}\mRightarrow{}  (l  \mbackslash{}/  n  \mvee{}  m  \mbackslash{}/  n)))
    {}\mRightarrow{}  (\mforall{}p,q,r:l,m:Line//l  ||  m.  \mforall{}P:\{P:Line|  p  =  P\}  .  \mforall{}Q:\{Q:Line|  q  =  Q\}  .  \mforall{}R:\{R:Line|  r  =  R\}  .
                (P  \mbackslash{}/  Q  {}\mRightarrow{}  (P  \mbackslash{}/  R  \mvee{}  Q  \mbackslash{}/  R))))


By

---

Latex:
Auto

---

Home Index