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