:: deftheorem defines conjugate_Classes WEDDWITT:def 3 :
for G being Group holds conjugate_Classes G = { (con_class a) where a is Element of G : verum } ;