thus 2 > 1 ; :: according to INT_2:def 5 :: thesis: for n being natural number holds
( not n divides 2 or n = 1 or n = 2 )
let n be natural number ; :: thesis: ( not n divides 2 or n = 1 or n = 2 )
assume A1: n divides 2 ; :: thesis: ( n = 1 or n = 2 )
then n <> 0 by Th3;
then n > 0 by NAT_1:3;
then A2: n >= 0 + 1 by NAT_1:13;
then n - 1 >= 1 - 1 by XREAL_1:11;
then reconsider m = n - 1 as Element of NAT by INT_1:16;
( m + 1 = 1 or m >= 1 ) by A2, NAT_1:8;
then A3: ( (n + (- 1)) + 1 = 1 or (n + (- 1)) + 1 >= 1 + 1 ) by XREAL_1:8;
n <= 2 by A1, Th43;
hence ( n = 1 or n = 2 ) by A3, XXREAL_0:1; :: thesis: verum