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