:: deftheorem defines ID GRCAT_1:def 26 :
for V being Group_DOMAIN
for G being Element of V holds ID G = ID G;