for G being Group
for H being Subgroup of G holds
( carr H in Left_Cosets H & carr H in Right_Cosets H )