:: deftheorem Def15 defines Left_Cosets GROUP_2:def 15 :
for G being Group
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 ) );