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