:: deftheorem Def5 defines Coset RUSUB_1:def 5 :
for V being RealUnitarySpace
for W being Subspace of V
for b₃ being Subset of V holds
( b₃ is Coset of W iff ex v being VECTOR of V st b₃ = v + W );