let C be compact Subset of (TOP-REAL 2); :: thesis: UBD C is_a_component_of C `
UBD C is_outside_component_of C by Th53;
hence UBD C is_a_component_of C ` ; :: thesis: verum