for C being Subset of (TOP-REAL 2) st C is bounded holds
not UBD C is empty by Lm13;