let V be RealLinearSpace; :: thesis: for M being non empty Subset of V holds 0. V in M - M
let M be non empty Subset of V; :: thesis: 0. V in M - M
consider v being object such that
A1: v in M by XBOOLE_0:def 1;
reconsider v = v as Element of V by A1;
v - v in { (u1 - v1) where u1, v1 is Element of V : ( u1 in M & v1 in M ) } by A1;
hence 0. V in M - M by RLVECT_1:15; :: thesis: verum