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:26;
reconsider n = n as Nat ;
consider x being set such that
A5: n = {x} by A1, A2, REALSET1:def 4;
A6: n = { k where k is Element of NAT : k < n } by AXIOMS:30;
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 A8: ( n = 0 or n = 1 ) ; :: thesis: n is trivial

per cases ( n = 0 or n = 1 ) by A8;

suppose n = 0 ; :: thesis: n is trivial

hence ( n is empty or ex x being set st n = {x} ) ; :: according to REALSET1:def 4 :: thesis: verum

end;

suppose A9: n = 1 ; :: thesis: n is trivial

A10: for x being set holds
( x in { k where k is Element of NAT : k < 1 } iff x in {0} )

proof

let x be set ; :: thesis: ( x in { k where k is Element of NAT : k < 1 } iff x in {0} )

hereby :: thesis: ( x in {0} implies x in { k where k is Element of NAT : k < 1 } )

assume x in { k where k is Element of NAT : k < 1 } ; :: thesis: x in {0}
then ex k being Element of NAT st
( x = k & k < 1 ) ;
then x = 0 by NAT_1:14;
hence x in {0} by TARSKI:def 1; :: thesis: verum

end;

assume x in {0} ; :: thesis: x in { k where k is Element of NAT : k < 1 }
then x = 0 by TARSKI:def 1;
hence x in { k where k is Element of NAT : k < 1 } ; :: thesis: verum

end;

1 = { k where k is Element of NAT : k < 1 } by AXIOMS:30;
then n = {0} by A9, A10, TARSKI:2;
hence ( n is empty or ex x being set st n = {x} ) ; :: according to REALSET1:def 4 :: thesis: verum

end;

end;