let K be Ring; :: thesis: for V being LeftMod of K
for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
let V be LeftMod of K; :: thesis: for W1, W2, W3 being Subspace of V holds (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
let W1, W2, W3 be Subspace of V; :: thesis: (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3)
(W1 /\ W2) + (W2 /\ W3) is Subspace of W2 /\ (W1 + W3) by VECTSP_5:26;
hence (W1 /\ W2) + (W2 /\ W3) c= W2 /\ (W1 + W3) by Def7; :: thesis: verum