per cases
( n is odd or n is even )
;

end;

suppose
n is odd
; :: thesis: ex b_{1} being natural number st

( b_{1} is n _greater & b_{1} is even )

( b

then consider k being Integer such that

A3: n = (2 * k) + 1 by ABIAN:1;

take n + 1 ; :: thesis: ( n + 1 is n _greater & n + 1 is even )

n + 1 > n + 0 by XREAL_1:6;

hence n + 1 is n _greater ; :: thesis: n + 1 is even

thus n + 1 is even by A3; :: thesis: verum

end;A3: n = (2 * k) + 1 by ABIAN:1;

take n + 1 ; :: thesis: ( n + 1 is n _greater & n + 1 is even )

n + 1 > n + 0 by XREAL_1:6;

hence n + 1 is n _greater ; :: thesis: n + 1 is even

thus n + 1 is even by A3; :: thesis: verum

suppose
n is even
; :: thesis: ex b_{1} being natural number st

( b_{1} is n _greater & b_{1} is even )

( b

then consider k being Nat such that

A4: n = 2 * k ;

take n + 2 ; :: thesis: ( n + 2 is n _greater & n + 2 is even )

n + 1 > n + 0 by XREAL_1:6;

hence n + 2 is n _greater by XREAL_1:6; :: thesis: n + 2 is even

thus n + 2 is even by A4; :: thesis: verum

end;A4: n = 2 * k ;

take n + 2 ; :: thesis: ( n + 2 is n _greater & n + 2 is even )

n + 1 > n + 0 by XREAL_1:6;

hence n + 2 is n _greater by XREAL_1:6; :: thesis: n + 2 is even

thus n + 2 is even by A4; :: thesis: verum