Theorem T000631

∧ ¬