:: deftheorem Def16 defines Right_Cosets GROUP_2:def 16 :
for G being Group
for H being Subgroup of G
for b₃ being Subset-Family of G holds
( b₃ = Right_Cosets H iff for A being Subset of G holds
( A in b₃ iff ex a being Element of G st A = H * a ) );