let a, b, c be Nat; :: thesis: ( (a + b) + c is odd & a,b,c are_mutually_coprime implies ( a is odd & b is odd & c is odd ) )
assume that
A1: (a + b) + c is odd and
A2: a,b,c are_mutually_coprime ; :: thesis: ( a is odd & b is odd & c is odd )
assume ( a is even or b is even or c is even ) ; :: thesis: contradiction

per cases then ( a is even or b is even or c is even ) ;

suppose A3: a is even ; :: thesis: contradiction

then ( ( b is odd & c is even ) or ( b is even & c is odd ) ) by A1;
then ( not a,c are_coprime or not a,b are_coprime ) by A3;
hence contradiction by A2; :: thesis: verum

end;

suppose A4: b is even ; :: thesis: contradiction

then ( ( a is odd & c is even ) or ( a is even & c is odd ) ) by A1;
then ( not b,c are_coprime or not b,a are_coprime ) by A4;
hence contradiction by A2; :: thesis: verum

end;

suppose A5: c is even ; :: thesis: contradiction

then ( ( a is odd & b is even ) or ( a is even & b is odd ) ) by A1;
then ( not c,b are_coprime or not c,a are_coprime ) by A5;
hence contradiction by A2; :: thesis: verum

end;

end;