theorem Th5: :: INT_2:5

for a, b being Integer holds
( ( a = 0 & b = 0 ) iff a gcd b = 0 )