---

Step * of Lemma geo-SCO_wf

∀[g:EuclideanPlaneStructure]
  ∀c,d,a:Point. ∀b:{b:Point| b ≠ a ∧ c_b_d} .  (SCO(a;b;c;d) ∈ {u:Point| cu ≅ cd ∧ a_b_u ∧ (b ≠ d ⇒ b ≠ u)} )
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}[g:EuclideanPlaneStructure]
    \mforall{}c,d,a:Point.  \mforall{}b:\{b:Point|  b  \mneq{}  a  \mwedge{}  c\_b\_d\}  .
        (SCO(a;b;c;d)  \mmember{}  \{u:Point|  cu  \mcong{}  cd  \mwedge{}  a\_b\_u  \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  b  \mneq{}  u)\}  )


By

---

Latex:
ProveWfLemma

---

Home Index