theorem Th63: :: GROUP_24:12

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