let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: for M being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF
for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let M be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; :: thesis: for W1, W2, W3 being Subspace of M st W1 is Subspace of W2 holds
W1 /\ W3 is Subspace of W2 /\ W3
let W1, W2, W3 be Subspace of M; :: thesis: ( W1 is Subspace of W2 implies W1 /\ W3 is Subspace of W2 /\ W3 )
set A1 = the carrier of W1;
set A2 = the carrier of W2;
set A3 = the carrier of W3;
set A4 = the carrier of (W1 /\ W3);
assume W1 is Subspace of W2 ; :: thesis: W1 /\ W3 is Subspace of W2 /\ W3
then the carrier of W1 c= the carrier of W2 by VECTSP_4:def 2;
then the carrier of W1 /\ the carrier of W3 c= the carrier of W2 /\ the carrier of W3 by XBOOLE_1:26;
then the carrier of (W1 /\ W3) c= the carrier of W2 /\ the carrier of W3 by Def2;
then the carrier of (W1 /\ W3) c= the carrier of (W2 /\ W3) by Def2;
hence W1 /\ W3 is Subspace of W2 /\ W3 by VECTSP_4:27; :: thesis: verum