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

`∀e:EuclideanStructure. ∀[a,b,c:Point].  (Colinear(a;b;c)) supposing (a-b-c and (¬(a = b ∈ Point)))`

Proof

Definitions occuring in Statement :  eu-colinear: `Colinear(a;b;c)` eu-between: `a-b-c` eu-point: `Point` euclidean-structure: `EuclideanStructure` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` equal: `s = t ∈ T`
Definitions unfolded in proof :  prop: `ℙ` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` false: `False` implies: `P `` Q` not: `¬A` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]`
Lemmas referenced :  eu-between-eq-implies-colinear eu-point_wf eu-between-eq-def and_wf not_wf equal_wf eu-between_wf euclidean-structure_wf
Rules used in proof :  independent_functionElimination productElimination independent_isectElimination rename equalityEquality voidElimination lambdaEquality sqequalRule introduction isectElimination isect_memberFormation hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution lemma_by_obid cut

Latex:
\mforall{}e:EuclideanStructure.  \mforall{}[a,b,c:Point].    (Colinear(a;b;c))  supposing  (a-b-c  and  (\mneg{}(a  =  b)))

Date html generated: 2016_05_18-AM-06_33_09
Last ObjectModification: 2016_01_03-PM-08_32_58

Theory : euclidean!geometry

Home Index