theorem :: GROUP_3:94

for x being set
for G being Group
for A being Subset of G holds
( x in con_class A iff ex B being Subset of G st
( x = B & A,B are_conjugated ) ) ;