Nuprl Lemma : outer-Pasch

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


Proof




Definitions occuring in Statement :  euclidean-plane: EuclideanPlane geo-strict-between: a-b-c geo-between: B(abc) geo-lsep: bc 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] sq_exists: x:A [B[x]] cand: c∧ B not: ¬A false: False stable: Stable{P} geo-eq: a ≡ b iff: ⇐⇒ Q 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 decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) select: L[n] cons: [a b] subtract: m geo-strict-between: a-b-c geo-colinear: Colinear(a;b;c) rev_implies:  Q

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{}  (\mexists{}p:Point  [(B(axp)  \mwedge{}  B(cpy))]))



Date html generated: 2020_05_20-AM-10_01_31
Last ObjectModification: 2019_12_03-AM-09_52_45

Theory : euclidean!plane!geometry


Home Index