for G being addGroup
for H being Subgroup of G st G is finite holds
( Right_Cosets H is finite & Left_Cosets H is finite ) ;