theorem Th23: :: INT_8:23

for m being Nat
for d, e being Element of NAT st d in dom (Sgm (RelPrimes m)) & e in dom (Sgm (RelPrimes m)) & d <> e holds
not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . e are_congruent_mod m