:: deftheorem defines con_class GROUP_1A:def 38 :
for G being addGroup
for A being Subset of G holds con_class A = { B where B is Subset of G : A,B are_conjugated } ;