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