:: deftheorem defines CosetSet ZMODUL02:def 6 :
for V being Z_Module
for W being Submodule of V holds CosetSet (V,W) = { A where A is Coset of W : verum } ;