### Nuprl Lemma : eu-not-equal-OXY

`∀[e:EuclideanStructure]. ((¬(O = X ∈ Point)) ∧ (¬(O = Y ∈ Point)) ∧ (¬(X = Y ∈ Point)))`

Proof

Definitions occuring in Statement :  eu-Y: `Y` eu-X: `X` eu-O: `O` eu-point: `Point` euclidean-structure: `EuclideanStructure` uall: `∀[x:A]. B[x]` not: `¬A` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` not: `¬A` implies: `P `` Q` false: `False` prop: `ℙ` all: `∀x:A. B[x]` cand: `A c∧ B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  eu-not-colinear-OXY equal_wf eu-point_wf eu-O_wf eu-X_wf eu-colinear_wf eu-Y_wf euclidean-structure_wf not_wf member_wf eu-between_wf eu-colinear-def
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality independent_pairFormation lambdaFormation productElimination independent_functionElimination voidElimination dependent_functionElimination equalitySymmetry hyp_replacement Error :applyLambdaEquality,  sqequalRule because_Cache equalityTransitivity productEquality

Latex:
\mforall{}[e:EuclideanStructure].  ((\mneg{}(O  =  X))  \mwedge{}  (\mneg{}(O  =  Y))  \mwedge{}  (\mneg{}(X  =  Y)))

Date html generated: 2016_10_26-AM-07_40_40
Last ObjectModification: 2016_07_12-AM-08_06_42

Theory : euclidean!geometry

Home Index