theorem :: GROUP_4:44
for G being Group
for H1, H2, H3 being Subgroup of G holds (H1 * H2) * H3 = H1 * (H2 * H3)