let C be compact Subset of ; :: 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