let a, b be Element of NAT ; :: thesis: ( not a,b are_relative_prime or not a is even or not b is even )
assume A1: a,b are_relative_prime ; :: thesis: ( not a is even or not b is even )
assume a is even ; :: thesis: not b is even
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