theorem Th135: :: GROUP_1A:181

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