let V be strict RealUnitarySpace; :: thesis: V in Subspaces V
(Omega). V in Subspaces V by Def3;
hence V in Subspaces V by RUSUB_1:def 3; :: thesis: verum