:: deftheorem defines CosetSet VECTSP10:def 2 :
for K being non empty right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr
for V being VectSp of K
for W being Subspace of V holds CosetSet (V,W) = { A where A is Coset of W : verum } ;