Nuprl Lemma : eu-between-implies-colinear

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


Definitions occuring in Statement :  eu-colinear: Colinear(a;b;c) eu-between: a-b-c eu-point: Point euclidean-structure: EuclideanStructure uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  prop: rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q false: False implies:  Q not: ¬A uimplies: 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

\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