not [#] (TOP-REAL n) is Bounded by JORDAN2C:41, NAT_1:14;
hence for b₁ being Subset of (TOP-REAL n) st b₁ is Bounded holds
b₁ is proper by SUBSET_1:def 7; :: thesis: verum