Nuprl Lemma : eu-colinear-same-side

  ∀[A,B,C,D:Point].  (Colinear(B;C;D)) supposing ((¬(B C ∈ Point)) and (A B ∈ Point)) and A_B_C and A_B_D)


Definitions occuring in Statement :  euclidean-plane: EuclideanPlane eu-between-eq: a_b_c eu-colinear: Colinear(a;b;c) eu-point: Point uimplies: supposing a uall: [x:A]. B[x] all: x:A. B[x] not: ¬A equal: t ∈ T
Definitions unfolded in proof :  prop: euclidean-plane: EuclideanPlane false: False implies:  Q not: ¬A uimplies: supposing a uall: [x:A]. B[x] member: t ∈ T all: x:A. B[x] rev_implies:  Q and: P ∧ Q iff: ⇐⇒ Q cand: c∧ B
Lemmas referenced :  eu-between-eq-def eu-colinear-def eu-between_wf eu-between-eq-same-side2 eu-point_wf not_wf equal_wf eu-between-eq_wf euclidean-plane_wf
Rules used in proof :  rename setElimination equalityEquality voidElimination lambdaEquality sqequalRule introduction independent_isectElimination isectElimination isect_memberFormation hypothesisEquality thin dependent_functionElimination sqequalHypSubstitution hypothesis lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution lemma_by_obid cut because_Cache productEquality independent_pairFormation independent_functionElimination productElimination equalitySymmetry

    \mforall{}[A,B,C,D:Point].    (Colinear(B;C;D))  supposing  ((\mneg{}(B  =  C))  and  (\mneg{}(A  =  B))  and  A\_B\_C  and  A\_B\_D)

Date html generated: 2016_05_18-AM-06_39_53
Last ObjectModification: 2016_01_01-PM-00_05_20

Theory : euclidean!geometry

Home Index