theorem :: GROUP_1A:293

for x being set
for G being addGroup
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 ) ) ;