UBD C is_outside_component_of C by Th76;
then A1: UBD C is_a_component_of C ` by Def4;
C ` <> {} by Th74;
hence not UBD C is empty by A1, SPRECT_1:6; :: thesis: verum