Nuprl Lemma : outer-pasch-strict

e:EuclideanPlane. ∀a,b:Point. ∀c:{c:Point| B(abc)} . ∀x:Point. ∀y:{y:Point| b-x-y} .
  (x ab   (∃p:Point [(a-x-p ∧ c-p-y)]))


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane geo-strict-between: a-b-c geo-between: B(abc) geo-lsep: bc geo-sep: b geo-point: Point all: x:A. B[x] sq_exists: x:A [B[x]] implies:  Q and: P ∧ Q set: {x:A| B[x]} 
Definitions unfolded in proof :  all: x:A. B[x] implies:  Q geo-lsep: bc or: P ∨ Q member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B guard: {T} uimplies: supposing a prop: euclidean-plane: EuclideanPlane sq_stable: SqStable(P) squash: T and: P ∧ Q oriented-plane: OrientedPlane basic-geometry-: BasicGeometry- exists: x:A. B[x] cand: c∧ B geo-colinear-set: geo-colinear-set(e; L) l_all: (∀x∈L.P[x]) top: Top int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) false: False select: L[n] cons: [a b] subtract: m basic-geometry: BasicGeometry sq_exists: x:A [B[x]] geo-strict-between: a-b-c stable: Stable{P} geo-eq: a ≡ b iff: ⇐⇒ Q geo-colinear: Colinear(a;b;c)

Latex:
\mforall{}e:EuclideanPlane.  \mforall{}a,b:Point.  \mforall{}c:\{c:Point|  B(abc)\}  .  \mforall{}x:Point.  \mforall{}y:\{y:Point|  b-x-y\}  .
    (x  \#  ab  {}\mRightarrow{}  b  \#  c  {}\mRightarrow{}  (\mexists{}p:Point  [(a-x-p  \mwedge{}  c-p-y)]))



Date html generated: 2020_05_20-AM-10_08_25
Last ObjectModification: 2019_12_03-AM-09_51_11

Theory : euclidean!plane!geometry


Home Index