let G be Group; :: thesis: for a being Element of G holds con_class {a} = { {b} where b is Element of G : b in con_class a }
let a be Element of G; :: thesis: con_class {a} = { {b} where b is Element of G : b in con_class a }
set A = { {b} where b is Element of G : b in con_class a } ;
thus con_class {a} c= { {b} where b is Element of G : b in con_class a } :: according to XBOOLE_0:def 10 :: thesis: { {b} where b is Element of G : b in con_class a } c= con_class {a}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in con_class {a} or x in { {b} where b is Element of G : b in con_class a } )
assume x in con_class {a} ; :: thesis: x in { {b} where b is Element of G : b in con_class a }
then consider B being Subset of G such that
A1: ( x = B & {a},B are_conjugated ) ;
consider b being Element of G such that
A2: {a} |^ b = B by A1, Th104;
A3: B = {(a |^ b)} by A2, Th44;
a,a |^ b are_conjugated by Th88;
then a |^ b in con_class a by Th96;
hence x in { {b} where b is Element of G : b in con_class a } by A1, A3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { {b} where b is Element of G : b in con_class a } or x in con_class {a} )
assume x in { {b} where b is Element of G : b in con_class a } ; :: thesis: x in con_class {a}
then consider b being Element of G such that
A4: ( x = {b} & b in con_class a ) ;
b,a are_conjugated by A4, Th96;
then {b},{a} are_conjugated by Th108;
hence x in con_class {a} by A4; :: thesis: verum