:: deftheorem defines con_class GROUP_3:def 8 :
for G being Group
for a being Element of G holds con_class a = a |^ (carr ((Omega). G));