Step * 2 of Lemma not_over_exists


1. Type
2. T ⟶ ℙ
3. ∀x:T. Q[x])
⊢ ¬(∃x:T. Q[x])
BY
(((D THENM (-1)) THENM With ⌜x⌝ (D 3)) THEN Auto) }


Latex:


Latex:

1.  T  :  Type
2.  Q  :  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  (\mneg{}Q[x])
\mvdash{}  \mneg{}(\mexists{}x:T.  Q[x])


By


Latex:
(((D  0  THENM  D  (-1))  THENM  With  \mkleeneopen{}x\mkleeneclose{}  (D  3))  THEN  Auto)




Home Index