let n be natural number ; :: thesis: ( n is empty or n = 1 or n > 1 )
assume not n is empty ; :: thesis: ( n = 1 or n > 1 )
then 0 + 1 <= n by Th13;
hence ( n = 1 or n > 1 ) by XXREAL_0:1; :: thesis: verum