theorem :: RLSUB_2:41

for V being RealLinearSpace holds
( (0). V is Linear_Compl of (Omega). V & (Omega). V is Linear_Compl of (0). V ) by Th39, Def5;