let a, b be Element of NAT ; :: thesis: ( not a,b are_relative_prime or a is odd or b is odd )
assume A1: a,b are_relative_prime ; :: thesis: ( a is odd or b is odd )
assume a is even ; :: thesis: b is odd
then A2: 2 divides a by PEPIN:22;
assume b is even ; :: thesis: contradiction
then 2 divides b by PEPIN:22;
hence contradiction by A1, A2, Def1; :: thesis: verum