theorem Th62: :: GROUP_24:11

for G being Group
for H1, H2 being Subgroup of G holds
( H1 * H2 c= the carrier of (H1 "\/" H2) & H2 * H1 c= the carrier of (H1 "\/" H2) )