A1: UBD C is_outside_component_of C by Th68;
thus not UBD C is empty by A1, Def3; :: thesis: verum