let H1, H2 be strict Subgroup of G; :: thesis: ( the carrier of H1 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } & the carrier of H2 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } implies H1 = H2 )
assume that
A1: the carrier of H1 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } and
A2: the carrier of H2 = { b where b is Element of G : for a being Element of G st a in A holds
a * b = b * a } ; :: thesis: H1 = H2
for g being Element of G holds
( g in H1 iff g in H2 ) by A1, A2;
hence H1 = H2 ; :: thesis: verum