let P be Subset of (TOP-REAL 2); :: thesis: ( P is Bounded implies not UBD P is Bounded )
assume P is Bounded ; :: thesis: not UBD P is Bounded
then UBD P is_outside_component_of P by JORDAN2C:68;
hence not UBD P is Bounded by JORDAN2C:def 3; :: thesis: verum