Nuprl Lemma : geo-proper-segment_wf

[e:EuclideanPlaneStructure]. (geo-proper-segment(e) ∈ Type)


Proof




Definitions occuring in Statement :  geo-proper-segment: geo-proper-segment(e) euclidean-plane-structure: EuclideanPlaneStructure uall: [x:A]. B[x] member: t ∈ T universe: Type
Definitions unfolded in proof :  prop: geo-proper-segment: geo-proper-segment(e) member: t ∈ T uall: [x:A]. B[x]
Lemmas referenced :  euclidean-plane-structure_wf geo-seg-proper_wf geo-segment_wf
Rules used in proof :  equalitySymmetry equalityTransitivity axiomEquality hypothesis hypothesisEquality thin isectElimination sqequalHypSubstitution extract_by_obid productEquality sqequalRule cut introduction isect_memberFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}[e:EuclideanPlaneStructure].  (geo-proper-segment(e)  \mmember{}  Type)



Date html generated: 2017_10_02-PM-04_44_37
Last ObjectModification: 2017_08_05-AM-09_27_07

Theory : euclidean!plane!geometry


Home Index