for V being RealLinearSpace
for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L