let G be Group; :: thesis: for H1, H2 being strict Subgroup of G holds
( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
let H1, H2 be strict Subgroup of G; :: thesis: ( con_class H1 = con_class H2 iff con_class H1 meets con_class H2 )
thus ( con_class H1 = con_class H2 implies con_class H1 meets con_class H2 ) :: thesis: ( con_class H1 meets con_class H2 implies con_class H1 = con_class H2 )

proof

assume con_class H1 = con_class H2 ; :: thesis: con_class H1 meets con_class H2
then ( H1 in con_class H2 & H1 in con_class H1 ) by Th130;
hence con_class H1 meets con_class H2 by XBOOLE_0:3; :: thesis: verum

end;

assume con_class H1 meets con_class H2 ; :: thesis: con_class H1 = con_class H2
then consider x being set such that
A1: ( x in con_class H1 & x in con_class H2 ) by XBOOLE_0:3;
reconsider x = x as strict Subgroup of G by A1, Th127;
thus con_class H1 c= con_class H2 :: according to XBOOLE_0:def 10 :: thesis: con_class H2 c= con_class H1

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in con_class H1 or y in con_class H2 )
assume y in con_class H1 ; :: thesis: y in con_class H2
then consider H3 being strict Subgroup of G such that
A2: ( H3 = y & H1,H3 are_conjugated ) by Def12;
( x,H1 are_conjugated & x,H2 are_conjugated ) by A1, Th128;
then ( x,H3 are_conjugated & H2,x are_conjugated ) by A2, Th124;
then H2,H3 are_conjugated by Th124;
hence y in con_class H2 by A2, Def12; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in con_class H2 or y in con_class H1 )
assume y in con_class H2 ; :: thesis: y in con_class H1
then consider H3 being strict Subgroup of G such that
A3: ( H3 = y & H2,H3 are_conjugated ) by Def12;
( x,H2 are_conjugated & x,H1 are_conjugated ) by A1, Th128;
then ( H1,x are_conjugated & x,H3 are_conjugated ) by A3, Th124;
then H1,H3 are_conjugated by Th124;
hence y in con_class H1 by A3, Def12; :: thesis: verum