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

( 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