Theorem T000645

∧ ¬