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