The mirror image of the inclusion rule. A prediction already in the list contributes $p · j$ to the numerator (probability $p$ of being matched, IoU $j$ when it is) and exactly $½$ to the denominator in both cases: removing a matched one turns a true positive into a false negative (net $−½$), removing an unmatched one deletes a false positive ($−½$). The score after removal is the exact quotient $pqWithoutPrediction$.

Removing the prediction raises the Panoptic Quality if and only if its contribution is below half the current score. The hypothesis $½ < den n fp fn$ says that something remains after the removal, so the new denominator is positive. The last statement closes the circuit with $Candidate$: removing what inclusion added returns the original score.