theorem Th37: :: GAUSSINT:37

for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & a is_associated_to b holds
aa is_associated_to bb