:: deftheorem defines con_class GROUP_3:def 10 :
for G being Group
for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;