### Nuprl Lemma : eu-colinear-from-between

`∀e:EuclideanPlane`
`  ∀[A,C,D:Point].  ((¬(A = C ∈ Point)) `` (∃B:Point. ((¬(A = B ∈ Point)) ∧ A_C_B ∧ A_D_B)) `` Colinear(A;C;D))`

Proof

Definitions occuring in Statement :  euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-colinear: `Colinear(a;b;c)` eu-point: `Point` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` equal: `s = t ∈ T`
Definitions unfolded in proof :  so_apply: `x[s]` so_lambda: `λ2x.t[x]` euclidean-plane: `EuclideanPlane` prop: `ℙ` uimplies: `b supposing a` member: `t ∈ T` and: `P ∧ Q` exists: `∃x:A. B[x]` implies: `P `` Q` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]`
Lemmas referenced :  eu-colinear-between exists_wf eu-point_wf and_wf not_wf equal_wf eu-between-eq_wf euclidean-plane_wf
Rules used in proof :  lambdaEquality sqequalRule rename setElimination hypothesis independent_isectElimination isectElimination hypothesisEquality dependent_functionElimination lemma_by_obid cut thin productElimination sqequalHypSubstitution isect_memberFormation lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}e:EuclideanPlane
\mforall{}[A,C,D:Point].    ((\mneg{}(A  =  C))  {}\mRightarrow{}  (\mexists{}B:Point.  ((\mneg{}(A  =  B))  \mwedge{}  A\_C\_B  \mwedge{}  A\_D\_B))  {}\mRightarrow{}  Colinear(A;C;D))

Date html generated: 2016_05_18-AM-06_40_06
Last ObjectModification: 2016_01_01-PM-00_40_58

Theory : euclidean!geometry

Home Index