let G be Group; :: thesis: for A, B being Subset of G holds
( con_class A = con_class B iff con_class A meets con_class B )
let A, B be Subset 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 ) ;
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 Subset 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 C being Subset of G such that
A2: ( C = y & A,C are_conjugated ) ;
( x,A are_conjugated & x,B are_conjugated ) by A1, Th113;
then ( x,C are_conjugated & B,x are_conjugated ) by A2, Th107;
then B,C are_conjugated by Th107;
hence y in con_class B by A2; :: 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 C being Subset of G such that
A3: ( C = y & B,C are_conjugated ) ;
( x,B are_conjugated & x,A are_conjugated ) by A1, Th113;
then ( A,x are_conjugated & x,C are_conjugated ) by A3, Th107;
then A,C are_conjugated by Th107;
hence y in con_class A by A3; :: thesis: verum