let R be Ring; :: thesis: for V being LeftMod of R
for W1, W2, W3 being Subspace of V st W1 /\ W2 <> (0). V holds
(W1 + W3) /\ W2 <> (0). V
let V be LeftMod of R; :: thesis: for W1, W2, W3 being Subspace of V st W1 /\ W2 <> (0). V holds
(W1 + W3) /\ W2 <> (0). V
let W1, W2, W3 be Subspace of V; :: thesis: ( W1 /\ W2 <> (0). V implies (W1 + W3) /\ W2 <> (0). V )
assume A1: W1 /\ W2 <> (0). V ; :: thesis: (W1 + W3) /\ W2 <> (0). V
consider v being Vector of V such that
A2: ( v in W1 /\ W2 & v <> 0. V ) by A1, ZMODUL04:24;
A3: ( v in W1 & v in W2 ) by A2, ZMODUL01:94;
then v in W1 + W3 by ZMODUL01:93;
hence (W1 + W3) /\ W2 <> (0). V by A2, ZMODUL02:66, A3, ZMODUL01:94; :: thesis: verum