theorem Lm89B: :: DUALSP04:38

for V being RealUnitarySpace
for W being Subspace of V
for v being VECTOR of V st v <> 0. V & v in Ort_Comp W holds
not v in W