let a, b, c be Integer; :: thesis: for r being Nat st r = numberR (a,b,c) holds
two_or_more_are_odd_among a + r,b + r,c + r
let r be Nat; :: thesis: ( r = numberR (a,b,c) implies two_or_more_are_odd_among a + r,b + r,c + r )
assume A1: r = numberR (a,b,c) ; :: thesis: two_or_more_are_odd_among a + r,b + r,c + r

per cases ( two_or_more_are_even_among a,b,c or not two_or_more_are_even_among a,b,c ) ;

suppose A2: two_or_more_are_even_among a,b,c ; :: thesis: two_or_more_are_odd_among a + r,b + r,c + r

then r = 1 by A1, Def9;
hence two_or_more_are_odd_among a + r,b + r,c + r by A2; :: thesis: verum

end;

suppose A3: not two_or_more_are_even_among a,b,c ; :: thesis: two_or_more_are_odd_among a + r,b + r,c + r

then r = 0 by A1, Def9;
hence two_or_more_are_odd_among a + r,b + r,c + r by A3; :: thesis: verum

end;

end;