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

( ((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