let x be non empty Nat; :: thesis: 0 in x
reconsider n = x as Element of NAT by ORDINAL1:def 13;
A1: n = { i where i is Element of NAT : i < n } by AXIOMS:30;
0 < n by NAT_1:3;
hence 0 in x by A1; :: thesis: verum