let G be Group; :: thesis: for a, b being Element of G holds
( con_class a = con_class b iff con_class a meets con_class b )
let a, b be Element of G; :: thesis: ( con_class a = con_class b iff con_class a meets con_class b )
thus ( con_class a = con_class b implies con_class a meets con_class b ) :: thesis: ( con_class a meets con_class b implies con_class a = con_class b )

proof

assume con_class a = con_class b ; :: thesis: con_class a meets con_class b
then ( a in con_class b & a in con_class a ) by Th96;
hence con_class a meets con_class b by XBOOLE_0:3; :: thesis: verum

end;

assume con_class a meets con_class b ; :: thesis: con_class a = con_class b
then consider x being set such that
A1: ( x in con_class a & x in con_class b ) by XBOOLE_0:3;
reconsider x = x as Element of G by A1;
thus con_class a c= con_class b :: according to XBOOLE_0:def 10 :: thesis: con_class b c= con_class a

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in con_class a or y in con_class b )
assume y in con_class a ; :: thesis: y in con_class b
then consider g being Element of G such that
A2: ( g = y & a,g are_conjugated ) by Th95;
( x,a are_conjugated & x,b are_conjugated ) by A1, Th96;
then ( x,g are_conjugated & b,x are_conjugated ) by A2, Th91;
then b,g are_conjugated by Th91;
hence y in con_class b by A2, Th95; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in con_class b or y in con_class a )
assume y in con_class b ; :: thesis: y in con_class a
then consider g being Element of G such that
A3: ( g = y & b,g are_conjugated ) by Th95;
( x,b are_conjugated & x,a are_conjugated ) by A1, Th96;
then ( a,x are_conjugated & x,g are_conjugated ) by A3, Th91;
then a,g are_conjugated by Th91;
hence y in con_class a by A3, Th95; :: thesis: verum