:: deftheorem Def15 defines Left_Cosets GROUP_1A:def 25 :
for G being addGroup
for H being Subgroup of G
for b₃ being Subset-Family of G holds
( b₃ = Left_Cosets H iff for A being Subset of G holds
( A in b₃ iff ex a being Element of G st A = a + H ) );