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 Th76;
hence UBD C is_a_component_of C ` by Def4; :: thesis: verum