let G be addGroup; :: 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 ) by Th109; :: thesis: ( con_class H1 meets con_class H2 implies con_class H1 = con_class H2 )
assume con_class H1 meets con_class H2 ; :: thesis: con_class H1 = con_class H2
then consider x being object such that
A1: x in con_class H1 and
A2: x in con_class H2 by XBOOLE_0:3;
reconsider x = x as strict Subgroup of G by A1, Th106;
A3: H1,x are_conjugated by A1, Th107;
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 object ; :: 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
A4: H3 = y and
A5: H1,H3 are_conjugated by Def12;
A6: H2,x are_conjugated by A2, Th107;
x,H1 are_conjugated by A1, Th107;
then x,H3 are_conjugated by A5, Th105;
then H2,H3 are_conjugated by A6, Th105;
hence y in con_class H2 by A4, Def12; :: thesis: verum
end;
let y be object ; :: 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
A7: H3 = y and
A8: H2,H3 are_conjugated by Def12;
x,H2 are_conjugated by A2, Th107;
then x,H3 are_conjugated by A8, Th105;
then H1,H3 are_conjugated by A3, Th105;
hence y in con_class H1 by A7, Def12; :: thesis: verum