let a, b, c, d be Nat; :: thesis: ( a * b,c * d are_coprime implies a,c are_coprime )
assume A1: a * b,c * d are_coprime ; :: thesis: 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; :: thesis: verum