Nuprl Lemma : lsep-inner-pasch-ext
∀e:OrientedPlane. ∀a,b:Point. ∀c:{c:Point| c # ab} . ∀p:{p:Point| a-p-c} . ∀q:{q:Point| b-q-c} .
(∃x:{Point| (b_x_p ∧ a_x_q)})
Proof
Definitions occuring in Statement :
oriented-plane: OrientedPlane,
geo-lsep: a # bc,
geo-strict-between: a-b-c,
geo-between: a_b_c,
geo-point: Point,
all: ∀x:A. B[x],
sq_exists: ∃x:{A| B[x]},
and: P ∧ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
member: t ∈ T,
lsep-inner-pasch,
sq_stable__geo-lsep,
record-select: r.x,
use-plane-sep,
sq_stable__and,
ifthenelse: if b then t else f fi
Lemmas referenced :
lsep-inner-pasch,
sq_stable__geo-lsep,
use-plane-sep,
sq_stable__and
Rules used in proof :
introduction,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
instantiate,
extract_by_obid,
hypothesis,
sqequalRule,
thin,
sqequalHypSubstitution,
equalityTransitivity,
equalitySymmetry
Latex:
\mforall{}e:OrientedPlane. \mforall{}a,b:Point. \mforall{}c:\{c:Point| c \# ab\} . \mforall{}p:\{p:Point| a-p-c\} . \mforall{}q:\{q:Point| b-q-c\} .
(\mexists{}x:\{Point| (b\_x\_p \mwedge{} a\_x\_q)\})
Date html generated:
2017_10_02-PM-04_48_18
Last ObjectModification:
2017_08_13-PM-08_35_13
Theory : euclidean!plane!geometry
Home
Index