Theorem T000317

∧ ¬