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 )

proof

let g be Element of G; :: thesis: ( g in H1 iff g in H2 )

hereby :: thesis: ( g in H2 implies g in H1 )

assume g in H1 ; :: thesis: g in H2
then g in the carrier of H1 by STRUCT_0:def 5;
hence g in H2 by A10, A11, STRUCT_0:def 5; :: thesis: verum

end;

now

assume g in H2 ; :: thesis: g in H1
then g in the carrier of H2 by STRUCT_0:def 5;
hence g in H1 by A10, A11, STRUCT_0:def 5; :: thesis: verum

end;

hence ( g in H2 implies g in H1 ) ; :: thesis: verum

end;

hence H1 = H2 by GROUP_2:def 6; :: thesis: verum