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 A2: ( n <> 0 & n <> 1 ) ; :: thesis: contradiction
then A3: n > 1 + 0 by NAT_1:26;
reconsider n = n as Nat ;
n = { k where k is Element of NAT : k < n } by AXIOMS:30;
then A4: ( 0 in n & 1 in n ) by A3;
consider x being set such that
A5: n = {x} by A1, A2, REALSET1:def 4;
( 0 = x & 1 = x ) by A4, A5, TARSKI:def 1;
hence contradiction ; :: thesis: verum

end;

assume A6: ( n = 0 or n = 1 ) ; :: thesis: n is trivial

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

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 A7: n = 1 ; :: thesis: n is trivial

A8: 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 A7, A8, TARSKI:2;
hence ( n is empty or ex x being set st n = {x} ) ; :: according to REALSET1:def 4 :: thesis: verum

end;

end;