A1: UBD C is_outside_component_of C by Th53;
thus not UBD C is empty by A1; :: thesis: verum