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