for G being Group
for H being Subgroup of G holds
( union (Left_Cosets H) = the carrier of G & union (Right_Cosets H) = the carrier of G )