let V be RealLinearSpace; :: thesis: for W1, W2 being Subspace of V holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
let W1, W2 be Subspace of V; :: thesis: ( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )
the carrier of (W1 /\ W2) c= the carrier of W1 by Lm4;
hence W1 /\ W2 is Subspace of W1 by RLSUB_1:28; :: thesis: W1 /\ W2 is Subspace of W2
the carrier of (W2 /\ W1) c= the carrier of W2 by Lm4;
then the carrier of (W1 /\ W2) c= the carrier of W2 by Th14;
hence W1 /\ W2 is Subspace of W2 by RLSUB_1:28; :: thesis: verum