Description: Conditional operator existence. (Contributed by NM, 21-Mar-2011) (Proof shortened by BJ, 1-Sep-2022)