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