Nuprl Lemma : geo-length_wf
∀[e:BasicGeometry]. ∀[s:geo-segment(e)].  (|s| ∈ Length)
Proof
Definitions occuring in Statement : 
geo-length: |s|
, 
geo-length-type: Length
, 
geo-segment: geo-segment(e)
, 
basic-geometry: BasicGeometry
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
Definitions unfolded in proof : 
basic-geometry: BasicGeometry
, 
subtype_rel: A ⊆r B
, 
member: t ∈ T
, 
uall: ∀[x:A]. B[x]
Lemmas referenced : 
basic-geometry_wf, 
geo-segment_wf, 
subtype-geo-length-type, 
geo-length_wf1
Rules used in proof : 
because_Cache, 
isect_memberEquality, 
rename, 
setElimination, 
equalitySymmetry, 
equalityTransitivity, 
axiomEquality, 
sqequalRule, 
applyEquality, 
hypothesis, 
hypothesisEquality, 
thin, 
isectElimination, 
sqequalHypSubstitution, 
extract_by_obid, 
cut, 
introduction, 
isect_memberFormation, 
sqequalReflexivity, 
computationStep, 
sqequalTransitivity, 
sqequalSubstitution
Latex:
\mforall{}[e:BasicGeometry].  \mforall{}[s:geo-segment(e)].    (|s|  \mmember{}  Length)
Date html generated:
2017_10_02-PM-04_51_49
Last ObjectModification:
2017_08_05-AM-09_09_58
Theory : euclidean!plane!geometry
Home
Index