theorem Th16: :: RLSUB_2:16

for V being RealLinearSpace
for W1, W2 being Subspace of V holds
( W1 /\ W2 is Subspace of W1 & W1 /\ W2 is Subspace of W2 )