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

suppose n is odd ; :: thesis: ex b₁ being Nat st
( b₁ is n _greater & b₁ is even )

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;

suppose n is even ; :: thesis: ex b₁ being Nat st
( b₁ is n _greater & b₁ is even )

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;

end;