theorem :: RLSUB_2:13

for V being RealLinearSpace
for W being strict Subspace of V holds W /\ W = W