let a, b, c be Element of INT ; :: thesis: ( c <> 0 & a = b mod c & b,c are_relative_prime implies a,c are_relative_prime )
assume A1: ( c <> 0 & a = b mod c & b,c are_relative_prime ) ; :: thesis: a,c are_relative_prime
then b gcd c = 1 by INT_2:def 3;
then a gcd c = 1 by A1, INT_4:14, LMLmTh4B;
hence a,c are_relative_prime by INT_2:def 3; :: thesis: verum