let a, c, b be Integer; ( a,c are_relative_prime & b,c are_relative_prime implies a * b,c are_relative_prime )
assume that
A1:
a,c are_relative_prime
and
A2:
b,c are_relative_prime
; a * b,c are_relative_prime
A3:
a gcd c = 1
by A1, Def4;
A4:
((a * b) gcd c) gcd a divides a
by Def3;
A5:
(a * b) gcd c divides c
by Def3;
((a * b) gcd c) gcd a divides (a * b) gcd c
by Def3;
then
((a * b) gcd c) gcd a divides c
by A5, Lm2;
then
((a * b) gcd c) gcd a divides 1
by A3, A4, Def3;
then
( ((a * b) gcd c) gcd a = 1 or ((a * b) gcd c) gcd a = - 1 )
by Th17;
then
a,(a * b) gcd c are_relative_prime
by Def4, NAT_1:2;
then A6:
(a * b) gcd c divides b
by Th31, Th40;
b gcd c = 1
by A2, Def4;
then
(a * b) gcd c divides 1
by A5, A6, Def3;
then
( (a * b) gcd c = 1 or (a * b) gcd c = - 1 )
by Th17;
hence
a * b,c are_relative_prime
by Def4, NAT_1:2; verum