theorem Th23: :: DUALSP06:23

for X being RealNormSpace
for x being Point of (DualSp X)
for M being non empty Subspace of X holds { ||.(x - m).|| where m is Point of (DualSp X) : m in Ort_Comp M } is non empty real-membered bounded_below set