let V be strict RealLinearSpace; :: thesis: V in Subspaces V
(Omega). V in Subspaces V by Def3;
hence V in Subspaces V ; :: thesis: verum