theorem Th23: :: JORDAN2C:36

for n being Nat st n >= 1 holds
UBD ({} (TOP-REAL n)) = REAL n