theorem Th18: :: RLSUB_2:18

for V being RealLinearSpace
for W being Subspace of V holds
( ((0). V) /\ W = (0). V & W /\ ((0). V) = (0). V )