theorem :: JORDAN1K:17

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