Step * of Lemma Konig_wf

∀[k:ℕ]. (Konig(k) ∈ ℙ)
BY
{ (Unfold `Konig` 0 THEN Auto) }


Latex:


\mforall{}[k:\mBbbN{}].  (Konig(k)  \mmember{}  \mBbbP{})


By

(Unfold  `Konig`  0  THEN  Auto)




Home Index