:: deftheorem Def6 defines Coset RLSUB_1:def 6 :
for V being RealLinearSpace
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 );