let a, b, c, d be Nat; ( a * b,c * d are_coprime implies a,c are_coprime )
assume A1:
a * b,c * d are_coprime
; a,c are_coprime
A3:
a gcd c divides a * b
by INT_2:2, INT_2:21;
a gcd c divides c * d
by INT_2:2, INT_2:21;
hence
a,c are_coprime
by A1, A3, WSIERP_1:15, INT_2:22; verum