### Nuprl Lemma : not-eu-between-same2

`∀e:EuclideanPlane. ∀[a,b:Point].  False supposing a-a-b`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-between: `a-b-c` eu-point: `Point` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` false: `False`
Definitions unfolded in proof :  all: `∀x:A. B[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` false: `False` prop: `ℙ` euclidean-plane: `EuclideanPlane`
Lemmas referenced :  euclidean-plane_wf eu-point_wf eu-between_wf not-eu-between-same eu-between-sym
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination because_Cache independent_isectElimination hypothesis voidElimination sqequalRule setElimination rename isect_memberEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}[a,b:Point].    False  supposing  a-a-b

Date html generated: 2016_05_18-AM-06_34_19
Last ObjectModification: 2016_01_05-PM-00_57_02

Theory : euclidean!geometry

Home Index