theorem Th5: :: GROUP_5:5

for x being set
for G being Group
for H1, H2 being Subgroup of G st H1 * H2 = H2 * H1 holds
( x in H1 "\/" H2 iff ex a, b being Element of G st
( x = a * b & a in H1 & b in H2 ) )