per cases ( n is even or n is odd ) ;
suppose n is even ; :: thesis: ex b1 being natural number st
( b1 is n _greater & b1 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 b1 being natural number st
( b1 is n _greater & b1 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;