### Nuprl Lemma : eu-le-pt_wf

`∀[e:EuclideanStructure]. ∀[a,b,c,d:Point].  (eu-le-pt(e;a;b;c;d) ∈ ℙ)`

Proof

Definitions occuring in Statement :  eu-le-pt: `eu-le-pt(e;a;b;c;d)` eu-point: `Point` euclidean-structure: `EuclideanStructure` uall: `∀[x:A]. B[x]` prop: `ℙ` member: `t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` eu-le-pt: `eu-le-pt(e;a;b;c;d)` so_lambda: `λ2x.t[x]` so_apply: `x[s]`
Lemmas referenced :  euclidean-structure_wf eu-congruent_wf eu-between-eq_wf and_wf eu-point_wf exists_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis lambdaEquality axiomEquality equalityTransitivity equalitySymmetry isect_memberEquality because_Cache

Latex:
\mforall{}[e:EuclideanStructure].  \mforall{}[a,b,c,d:Point].    (eu-le-pt(e;a;b;c;d)  \mmember{}  \mBbbP{})

Date html generated: 2016_05_18-AM-06_43_28
Last ObjectModification: 2016_02_19-PM-02_31_38

Theory : euclidean!geometry

Home Index