let x be non empty Nat; :: thesis: 0 in x
reconsider n = x as Element of NAT by ORDINAL1:def 12;
( n = { i where i is Element of NAT : i < n } & 0 < n ) by AXIOMS:4, NAT_1:3;
hence 0 in x ; :: thesis: verum