let V be RealUnitarySpace; :: thesis: for W being strict Subspace of V holds
( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
let W be strict Subspace of V; :: thesis: ( ((Omega). V) /\ W = W & W /\ ((Omega). V) = W )
(Omega). V = UNITSTR(# the carrier of V, the ZeroF of V, the U7 of V, the Mult of V, the scalar of V #) by RUSUB_1:def 3;
then A1: the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W by Def2;
the carrier of W c= the carrier of V by RUSUB_1:def 1;
hence ((Omega). V) /\ W = W by A1, RUSUB_1:24, XBOOLE_1:28; :: thesis: W /\ ((Omega). V) = W
hence W /\ ((Omega). V) = W by Th14; :: thesis: verum