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 ) by Th81; :: thesis: ( con_class a meets con_class b implies con_class a = con_class b )
assume con_class a meets con_class b ; :: thesis: con_class a = con_class b
then consider x being object such that
A1: x in con_class a and
A2: x in con_class b by XBOOLE_0:3;
reconsider x = x as Element of G by A1;
A3: a,x are_conjugated by A1, Th81;
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 object ; :: 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
A4: g = y and
A5: a,g are_conjugated by Th80;
A6: b,x are_conjugated by A2, Th81;
x,a are_conjugated by A1, Th81;
then x,g are_conjugated by A5, Th77;
then b,g are_conjugated by A6, Th77;
hence y in con_class b by A4, Th80; :: thesis: verum
end;
let y be object ; :: 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
A7: g = y and
A8: b,g are_conjugated by Th80;
x,b are_conjugated by A2, Th81;
then x,g are_conjugated by A8, Th77;
then a,g are_conjugated by A3, Th77;
hence y in con_class a by A7, Th80; :: thesis: verum