Theorem Verification of the Quantifier-Guided Dominance Degree with the Mean Operator for Additive Preference Relations