let n be natural number ; :: thesis: ( ( n = 1 or n > 1 ) iff not n is empty )

hereby :: thesis: ( ( n = 1 or n > 1 ) implies not n is empty )

assume not n is empty ; :: thesis: ( n = 1 or n > 1 )
then 0 < n ;
then 0 + 1 <= n by NAT_1:13;
hence ( n = 1 or n > 1 ) by XXREAL_0:1; :: thesis: verum

end;

assume ( n = 1 or n > 1 ) ; :: thesis: not n is empty
hence not n is empty ; :: thesis: verum