theorem Th22: :: JORDAN2C:35
for n being Nat st n >= 1 holds
not [#] (TOP-REAL n) is bounded