Nuprl Lemma : geo-SS_wf
∀[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)} )
Proof
Error : references
Latex:
\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)\} )
Date html generated:
2020_05_21-AM-10_24_52
Last ObjectModification:
2019_12_03-AM-09_53_22
Theory : euclidean!plane!geometry
Home
Index