theorem :: RLSUB_2:24

for V being RealLinearSpace
for W2 being Subspace of V
for W1 being strict Subspace of V holds W1 /\ (W1 + W2) = W1 by Lm7, RLSUB_1:30;