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 A1: con_class a = con_class b ; :: thesis: con_class a meets con_class b
a in con_class a by Th96;
hence con_class a meets con_class b by A1, 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
A2: x in con_class a and
A3: x in con_class b by XBOOLE_0:3;
reconsider x = x as Element of G by A2;
A4: a,x are_conjugated by A2, Th96;
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
A5: g = y and
A6: a,g are_conjugated by Th95;
A7: b,x are_conjugated by A3, Th96;
x,a are_conjugated by A2, Th96;
then x,g are_conjugated by A6, Th91;
then b,g are_conjugated by A7, Th91;
hence y in con_class b by A5, 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
A8: g = y and
A9: b,g are_conjugated by Th95;
x,b are_conjugated by A3, Th96;
then x,g are_conjugated by A9, Th91;
then a,g are_conjugated by A4, Th91;
hence y in con_class a by A8, Th95; :: thesis: verum