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