theorem :: JORDAN1K:18

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