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 A1: con_class H1 = con_class H2 ; :: thesis: con_class H1 meets con_class H2
H1 in con_class H1 by Th130;
hence con_class H1 meets con_class H2 by A1, 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
A2: x in con_class H1 and
A3: x in con_class H2 by XBOOLE_0:3;
reconsider x = x as strict Subgroup of G by A2, Th127;
A4: H1,x are_conjugated by A2, Th128;
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
A5: H3 = y and
A6: H1,H3 are_conjugated by Def12;
A7: H2,x are_conjugated by A3, Th128;
x,H1 are_conjugated by A2, Th128;
then x,H3 are_conjugated by A6, Th124;
then H2,H3 are_conjugated by A7, Th124;
hence y in con_class H2 by A5, 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
A8: H3 = y and
A9: H2,H3 are_conjugated by Def12;
x,H2 are_conjugated by A3, Th128;
then x,H3 are_conjugated by A9, Th124;
then H1,H3 are_conjugated by A4, Th124;
hence y in con_class H1 by A8, Def12; :: thesis: verum