Nuprl Lemma : eu-mk-seg_wf

[e:EuclideanStructure]. ∀[a,b:Point].  (ab ∈ Segment)


Proof




Definitions occuring in Statement :  eu-mk-seg: ab eu-segment: Segment eu-point: Point euclidean-structure: EuclideanStructure uall: [x:A]. B[x] member: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T eu-mk-seg: ab subtype_rel: A ⊆B eu-segment: Segment
Lemmas referenced :  eu-point_wf euclidean-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule independent_pairEquality hypothesisEquality hypothesis applyEquality lambdaEquality sqequalHypSubstitution productEquality lemma_by_obid isectElimination thin axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b:Point].    (ab  \mmember{}  Segment)



Date html generated: 2016_05_18-AM-06_36_14
Last ObjectModification: 2015_12_28-AM-09_26_07

Theory : euclidean!geometry


Home Index