Theorem T000672

∧ ¬