theorem Th5: :: SF_MASTR:5

for a1, a2, b1, b2 being Int-Location st Divide (a1,b1) = Divide (a2,b2) holds
( a1 = a2 & b1 = b2 )