Step 
*
 of Lemma 
double-negation-shift_wf
∀A:ℕ ⟶ ℙ. (DNSi.A[i] ∈ ℙ)
BY
 
{ ProveWfLemma }
 
Latex: 
Latex:
\mforall{}A:\mBbbN{}  {}\mrightarrow{}  \mBbbP{}.  (DNSi.A[i]  \mmember{}  \mBbbP{})
 By 
Latex:
ProveWfLemma
Home
Index