:: deftheorem Def41 defines Cosets AIMLOOP:def 43 :
for Q being multLoop
for N being SubLoop of Q
for b₃ being Subset-Family of Q holds
( b₃ = Cosets N iff for H being Subset of Q holds
( H in b₃ iff ex x being Element of Q st H = x * N ) );