:: deftheorem defines Double_Cosets GROUP_8:def 1 :
for G being strict Group
for H, K being strict Subgroup of G
for b₄ being Subset-Family of G holds
( b₄ = Double_Cosets (H,K) iff for A being Subset of G holds
( A in b₄ iff ex a being Element of G st A = (H * a) * K ) );