theorem Th51: :: JORDAN2C:66
for n being Nat
for A being Subset of (TOP-REAL n) st 1 <= n & A is bounded holds
A ` <> {}