---

Step * of Lemma geo-SS_wf

No Annotations
∀[g:EuclideanPlaneStructure]. ∀[a,b:Point]. ∀[u:{u:Point| u leftof ab} ]. ∀[v:{v:Point| v leftof ba} ].
  (geo-SS(g;a;b;u;v) ∈ {x:Point| Colinear(a;b;x) ∧ B(uxv)} )
BY
{ ((ProveWfLemma THEN D 1) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[g:EuclideanPlaneStructure].  \mforall{}[a,b:Point].  \mforall{}[u:\{u:Point|  u  leftof  ab\}  ].
\mforall{}[v:\{v:Point|  v  leftof  ba\}  ].
    (geo-SS(g;a;b;u;v)  \mmember{}  \{x:Point|  Colinear(a;b;x)  \mwedge{}  B(uxv)\}  )


By

---

Latex:
((ProveWfLemma  THEN  D  1)  THEN  Auto)

---

Home Index