let V be RealLinearSpace; :: 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 )
( the carrier of (((Omega). V) /\ W) = the carrier of V /\ the carrier of W & the carrier of W c= the carrier of V ) by Def2, RLSUB_1:def 2;
hence ((Omega). V) /\ W = W by RLSUB_1:30, XBOOLE_1:28; :: thesis: W /\ ((Omega). V) = W
hence W /\ ((Omega). V) = W by Th14; :: thesis: verum