Nuprl Lemma : left-between-triangle2

e:EuclideanPlane. ∀a,x,y,p:Point.  (a leftof yx  x-p-a  leftof yp)


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane geo-strict-between: a-b-c geo-left: leftof bc geo-point: Point all: x:A. B[x] implies:  Q
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q member: t ∈ T prop: uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a geo-lsep: bc or: P ∨ Q and: P ∧ Q cand: c∧ B basic-geometry: BasicGeometry geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) top: Top int_seg: {i..j-} lelt: i ≤ j < k le: A ≤ B less_than': less_than'(a;b) false: False not: ¬A less_than: a < b squash: T true: True select: L[n] cons: [a b] subtract: m oriented-plane: OrientedPlane basic-geometry-: BasicGeometry-
Lemmas referenced :  geo-strict-between_wf euclidean-plane-structure-subtype euclidean-plane-subtype subtype_rel_transitivity euclidean-plane_wf euclidean-plane-structure_wf geo-primitives_wf geo-left_wf geo-point_wf left-convex geo-strict-between-implies-between geo-sep-sym geo-strict-between-sep2 geo-between_wf colinear-lsep lsep-all-sym geo-strict-between-sep3 geo-colinear-is-colinear-set geo-strict-between-implies-colinear length_of_cons_lemma length_of_nil_lemma false_wf lelt_wf left-between-implies-right2 geo-between-symmetry left-symmetry not-left-and-right
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality applyEquality hypothesis instantiate independent_isectElimination sqequalRule because_Cache inrFormation dependent_functionElimination independent_functionElimination independent_pairFormation productElimination isect_memberEquality voidElimination voidEquality dependent_set_memberEquality natural_numberEquality imageMemberEquality baseClosed unionElimination

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,x,y,p:Point.    (a  leftof  yx  {}\mRightarrow{}  x-p-a  {}\mRightarrow{}  a  leftof  yp)



Date html generated: 2017_10_02-PM-06_47_39
Last ObjectModification: 2017_09_13-PM-01_58_18

Theory : euclidean!plane!geometry


Home Index