thus
2 > 1
; :: according to INT_2:def 4 :: thesis: for n being Nat holds

( not n divides 2 or n = 1 or n = 2 )

let n be Nat; :: 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 Th27;

then not not n = 0 & ... & not n = 2 ;

hence ( n = 1 or n = 2 ) by A1; :: thesis: verum

( not n divides 2 or n = 1 or n = 2 )

let n be Nat; :: 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 Th27;

then not not n = 0 & ... & not n = 2 ;

hence ( n = 1 or n = 2 ) by A1; :: thesis: verum