theorem Th1: :: MATRLIN2:1

for K being Field
for V being VectSp of K
for W1, W2, W12 being Subspace of V
for U1, U2 being Subspace of W12 st U1 = W1 & U2 = W2 holds
( W1 /\ W2 = U1 /\ U2 & W1 + W2 = U1 + U2 )