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