for F being Field
for V being VectSp of F
for W being Subspace of V
for L being Linear_Compl of W holds W is Linear_Compl of L