theorem Th22: :: GROUP_9:22

for O being set
for G being GroupWithOperators of O
for N being normal StableSubgroup of G holds union (Cosets N) = the carrier of G