Nuprl Lemma : not-not-inner-pasch
∀g:OrientedPlane. ∀a,b,c:Point. ∀p:{p:Point| B(apc)} . ∀q:{q:Point| B(bqc)} . (¬¬(∃x:Point. (B(pxb) ∧ B(qxa))))
Proof
Definitions occuring in Statement :
oriented-plane: OrientedPlane,
geo-between: B(abc),
geo-point: Point,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
not: ¬A,
and: P ∧ Q,
set: {x:A| B[x]}
Definitions unfolded in proof :
cand: A c∧ B,
oriented-plane: OrientedPlane,
or: P ∨ Q,
prop: ℙ,
uimplies: b supposing a,
guard: {T},
subtype_rel: A ⊆r B,
uall: ∀[x:A]. B[x],
and: P ∧ Q,
member: t ∈ T,
exists: ∃x:A. B[x],
false: False,
implies: P ⇒ Q,
not: ¬A,
all: ∀x:A. B[x],
stable: Stable{P},
geo-eq: a ≡ b,
rev_implies: P ⇐ Q,
iff: P ⇐⇒ Q,
geo-strict-between: a-b-c,
squash: ↓T,
geo-between: B(abc),
sq_stable: SqStable(P),
euclidean-plane: EuclideanPlane,
sq_exists: ∃x:A [B[x]],
geo-colinear: Colinear(a;b;c),
basic-geometry-: BasicGeometry-
Latex:
\mforall{}g:OrientedPlane. \mforall{}a,b,c:Point. \mforall{}p:\{p:Point| B(apc)\} . \mforall{}q:\{q:Point| B(bqc)\} .
(\mneg{}\mneg{}(\mexists{}x:Point. (B(pxb) \mwedge{} B(qxa))))
Date html generated:
2020_05_20-AM-09_50_34
Last ObjectModification:
2019_12_20-PM-08_46_04
Theory : euclidean!plane!geometry
Home
Index