let n be non zero Nat; :: thesis: n is with_zero
{} in n by ORDINAL3:8;
hence n is with_zero ; :: thesis: verum