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 object ; :: 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 and
A2: {a},B are_conjugated ;
consider b being Element of G such that
A3: {a} |^ b = B by A2, Th88;
a,a |^ b are_conjugated by Th74;
then A4: a |^ b in con_class a by Th81;
B = {(a |^ b)} by A3, Th37;
hence x in { {b} where b is Element of G : b in con_class a } by A1, A4; :: thesis: verum
end;
let x be object ; :: 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
A5: x = {b} and
A6: b in con_class a ;
b,a are_conjugated by A6, Th81;
then {b},{a} are_conjugated by Th92;
hence x in con_class {a} by A5; :: thesis: verum