take the non zero Nat ; :: thesis: not the non zero Nat is limit_ordinal
thus not the non zero Nat is limit_ordinal ; :: thesis: verum