assume A1: n is trivial ; :: thesis:
assume that
A2: n <> 0 and
A3: n <> 1 ; :: thesis:
A4: n > 1 + 0 by A2, A3, NAT_1:25;
reconsider n = n as Nat ;
consider x being object such that
A5: n = {x} by A1, A2, ZFMISC_1:131;
A6: n = { k where k is Nat : k < n } by AXIOMS:4;
then A7: 1 in n by A4;
0 in n by A2, A6;
then 0 = x by A5, TARSKI:def 1;
hence contradiction by A7, A5, TARSKI:def 1; :: thesis:

end;