for V being strict RealLinearSpace
for W being strict Subspace of V st ( for v being VECTOR of V holds
( v in W iff v in V ) ) holds
W = V