let a, b, c be Nat; :: thesis: ( a <> 0 & b <> 0 & c <> 0 & c divides a * b & a,c are_relative_prime implies c divides b )
assume A1: ( a <> 0 & b <> 0 & c <> 0 & c divides a * b & a,c are_relative_prime ) ; :: thesis: c divides b
then a gcd c = 1 by INT_2:def 4;
then A2: (a * b) gcd (c * b) = b by Th6;
c divides c * b by NAT_D:9;
hence c divides b by A1, A2, NEWTON:63; :: thesis: verum