Nuprl Lemma : heyting-not-not-inner-pasch
∀e:HeytingGeometry. ∀a,b,c:Point. ∀p:{p:Point| a_p_c} . ∀q:{q:Point| b_q_c} . (¬¬(∃x:Point. (p_x_b ∧ q_x_a)))
Proof
Definitions occuring in Statement :
heyting-geometry: HeytingGeometry,
geo-between: a_b_c,
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 :
oriented-plane: OrientedPlane,
euclidean-plane: EuclideanPlane,
heyting-geometry: HeytingGeometry
Lemmas referenced :
not-not-inner-pasch
Rules used in proof :
hypothesis,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
sqequalRule,
extract_by_obid,
introduction,
cut
Latex:
\mforall{}e:HeytingGeometry. \mforall{}a,b,c:Point. \mforall{}p:\{p:Point| a\_p\_c\} . \mforall{}q:\{q:Point| b\_q\_c\} .
(\mneg{}\mneg{}(\mexists{}x:Point. (p\_x\_b \mwedge{} q\_x\_a)))
Date html generated:
2017_10_02-PM-07_01_13
Last ObjectModification:
2017_08_06-PM-09_15_03
Theory : euclidean!plane!geometry
Home
Index