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

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