theorem Th17: :: RLSUB_2:17

for V being RealLinearSpace
for W2 being Subspace of V
for W1 being strict Subspace of V holds
( W1 is Subspace of W2 iff W1 /\ W2 = W1 )