let k be Integer; :: thesis: 1,k are_relative_prime
1 gcd k = 1 by Th13;
hence 1,k are_relative_prime by INT_2:def 3; :: thesis: verum