theorem Th19: :: DUALSP06:19

for X being RealNormSpace
for x being Point of X
for M being non empty Subspace of X holds { (x .|. y) where y is Point of (DualSp X) : ( y in Ort_Comp M & ||.y.|| <= 1 ) } is non empty real-membered bounded_above set