let x be set ; :: thesis: for G being Group
for a being Element of G holds
( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
let G be Group; :: thesis: for a being Element of G holds
( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
let a be Element of G; :: thesis: ( x in con_class a iff ex b being Element of G st
( b = x & a,b are_conjugated ) )
thus ( x in con_class a implies ex b being Element of G st
( b = x & a,b are_conjugated ) ) :: thesis: ( ex b being Element of G st
( b = x & a,b are_conjugated ) implies x in con_class a )

proof

assume x in con_class a ; :: thesis: ex b being Element of G st
( b = x & a,b are_conjugated )
then x in { b where b is Element of G : a,b are_conjugated } by Th79;
hence ex b being Element of G st
( b = x & a,b are_conjugated ) ; :: thesis: verum

end;

given b being Element of G such that A1: ( b = x & a,b are_conjugated ) ; :: thesis: x in con_class a
x in { c where c is Element of G : a,c are_conjugated } by A1;
hence x in con_class a by Th79; :: thesis: verum