let a, b be Element of NAT ; :: thesis: ( not a,b are_relative_prime or a > 0 or b > 0 )
assume a,b are_relative_prime ; :: thesis: ( a > 0 or b > 0 )
then ( not a is even or not b is even ) by PYTHTRIP:10;
hence ( a > 0 or b > 0 ) by ABIAN:12; :: thesis: verum