thus 2 > 1 ; :: according to INT_2:def 4 :: thesis: for b₁ being set holds
( not R17(b₁,2) or b₁ = 1 or b₁ = 2 )
let n be Nat; :: thesis: ( not R17(n,2) or n = 1 or n = 2 )
assume A1: n divides 2 ; :: thesis: ( n = 1 or n = 2 )
then n <= 2 by INT_2:27;
then not not n = 0 & ... & not n = 2 ;
hence ( n = 1 or n = 2 ) by A1, INT_2:3; :: thesis: verum