:: deftheorem defines ID RINGCAT1:def 18 :
for V being Ring_DOMAIN
for G being Element of V holds ID G = ID G;