thus ( not n is trivial or n = 0 or n = 1 ) :: thesis: ( ( n = 0 or n = 1 ) implies n is trivial )

proof

assume A1: n is trivial ; :: thesis: ( n = 0 or n = 1 )
assume that
A2: n <> 0 and
A3: n <> 1 ; :: thesis: contradiction
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: verum

end;

assume ( n = 0 or n = 1 ) ; :: thesis: n is trivial
hence n is trivial by CARD_1:49; :: thesis: verum