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

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

then consider k being Nat such that
A1: n = 2 * k ;
take n + 1 ; :: thesis: ( n + 1 is n _greater & n + 1 is odd )
n + 1 > n + 0 by XREAL_1:6;
hence n + 1 is n _greater ; :: thesis: n + 1 is odd
thus n + 1 is odd by A1; :: thesis: verum

end;

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

then consider k being Integer such that
A2: n = (2 * k) + 1 by ABIAN:1;
take n + 2 ; :: thesis: ( n + 2 is n _greater & n + 2 is odd )
n + 1 > n + 0 by XREAL_1:6;
hence n + 2 is n _greater by XREAL_1:6; :: thesis: n + 2 is odd
thus n + 2 is odd by A2; :: thesis: verum

end;

end;