let n be natural Number ; :: thesis: ( not n <= 1 or n = 0 or n = 1 )
assume A1: n <= 1 ; :: thesis: ( n = 0 or n = 1 )
assume that
A2: not n = 0 and
A3: not n = 1 ; :: thesis: contradiction
n < 0 + 1 by A1, A3, XXREAL_0:1;
hence contradiction by A2, Th13; :: thesis: verum