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
A12: the carrier of H1 = { b where b is Element of G : a * b = b * a } and
A13: 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;
then consider b being Element of G such that
A14: b = g and
A15: a * b = b * a by A12;
g in the carrier of H2 by A13, A14, A15;
hence g in H2 by 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;
then consider b being Element of G such that
A16: b = g and
A17: a * b = b * a by A13;
g in the carrier of H1 by A12, A16, A17;
hence g in H1 by 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