theorem :: MOD_4:25

for K being Ring holds
( id K is antiisomorphism iff K is comRing )