thus 2 > 1 ; :: according to INT_2:def 4 :: 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 <= 2 by Th43;
then ( n = 0 or n = 1 or n = 2 ) by NAT_1:26;
hence ( n = 1 or n = 2 ) by A1, Th3; :: thesis: verum