### Nuprl Lemma : not-not-inner-pasch

`∀e:EuclideanPlane. ∀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 :  euclidean-plane: `EuclideanPlane` eu-between-eq: `a_b_c` eu-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 :  all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` false: `False` member: `t ∈ T` prop: `ℙ` uall: `∀[x:A]. B[x]` euclidean-plane: `EuclideanPlane` so_lambda: `λ2x.t[x]` and: `P ∧ Q` so_apply: `x[s]` stable: `Stable{P}` uimplies: `b supposing a` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` subtype_rel: `A ⊆r B` cand: `A c∧ B` rev_implies: `P `` Q`
Lemmas referenced :  not_wf exists_wf eu-point_wf eu-between-eq_wf set_wf euclidean-plane_wf eu-colinear-cases equal_wf eu-between_wf eu-colinear_wf dneg_elim_a all_wf stable_wf eu-between-eq-same eu-between-eq-symmetry eu-between-eq-trivial-left eu-between-eq-trivial-right eu-between-implies-between-eq eu-between-eq-exchange3 eu-between-eq-inner-trans eu-between-eq-exchange4 eu-between-eq-def eu-inner-pasch-property eu-inner-pasch_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin setElimination rename hypothesis sqequalHypSubstitution independent_functionElimination voidElimination introduction extract_by_obid isectElimination because_Cache sqequalRule lambdaEquality productEquality hypothesisEquality dependent_functionElimination isect_memberFormation equalityEquality addLevel impliesFunctionality productElimination levelHypothesis equalitySymmetry hyp_replacement Error :applyLambdaEquality,  instantiate universeEquality functionEquality applyEquality cumulativity independent_isectElimination dependent_pairFormation independent_pairFormation promote_hyp dependent_set_memberEquality

Latex:
\mforall{}e:EuclideanPlane.  \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: 2016_10_26-AM-07_41_25
Last ObjectModification: 2016_07_12-AM-08_08_24

Theory : euclidean!geometry

Home Index