### Nuprl Lemma : euclidean-point-eq

`∀[e:EuclideanPlane]. ∀[p,q:Point].  p = q ∈ Point supposing ¬¬(p = q ∈ Point)`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-point: `Point` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` stable: `Stable{P}` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` euclidean-plane: `EuclideanPlane`
Lemmas referenced :  stable_point-eq not_wf equal_wf eu-point_wf euclidean-plane_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis independent_isectElimination lambdaFormation independent_functionElimination voidElimination setElimination rename sqequalRule isect_memberEquality axiomEquality because_Cache equalityTransitivity equalitySymmetry

Latex:
\mforall{}[e:EuclideanPlane].  \mforall{}[p,q:Point].    p  =  q  supposing  \mneg{}\mneg{}(p  =  q)

Date html generated: 2016_05_18-AM-06_34_05
Last ObjectModification: 2015_12_28-AM-09_27_29

Theory : euclidean!geometry

Home Index