Nuprl Lemma : lsep-inner-pasch-strict-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-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-strict,
sq_stable__and,
lsep-inner-pasch-ext,
ifthenelse: if b then t else f fi
Lemmas referenced :
lsep-inner-pasch-strict,
sq_stable__and,
lsep-inner-pasch-ext
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_27
Last ObjectModification:
2017_08_13-PM-11_39_20
Theory : euclidean!plane!geometry
Home
Index