let n be Nat; :: thesis: ( not n <= 1 or n = 0 or n = 1 )
assume A1: n <= 1 ; :: thesis: ( n = 0 or n = 1 )
assume A2: ( not n = 0 & not n = 1 ) ; :: thesis: contradiction
then n < 0 + 1 by A1, XXREAL_0:1;
hence contradiction by A2, Th13; :: thesis: verum