Nuprl Lemma : eu-X_wf

`∀e:EuclideanStructure. (X ∈ Point)`

Proof

Definitions occuring in Statement :  eu-X: `X` eu-point: `Point` euclidean-structure: `EuclideanStructure` all: `∀x:A. B[x]` member: `t ∈ T`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` eu-X: `X` uall: `∀[x:A]. B[x]` spreadn: spread3 and: `P ∧ Q` prop: `ℙ` implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top`
Lemmas referenced :  eu-nontrivial_wf eu-point_wf not_wf equal_wf eu-colinear_wf pi1_wf_top pi2_wf subtype_rel_product top_wf euclidean-structure_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis setEquality productEquality because_Cache productElimination sqequalRule lambdaEquality setElimination rename applyEquality independent_isectElimination isect_memberEquality voidElimination voidEquality equalityEquality equalityTransitivity equalitySymmetry dependent_functionElimination independent_functionElimination

Latex:
\mforall{}e:EuclideanStructure.  (X  \mmember{}  Point)

Date html generated: 2016_05_18-AM-06_32_38
Last ObjectModification: 2015_12_28-AM-09_28_13

Theory : euclidean!geometry

Home Index