:: deftheorem defines CosetSet NORMSP_3:def 13 :
for X being RealLinearSpace
for Y being Subspace of X holds CosetSet (X,Y) = { A where A is Coset of Y : verum } ;