Theorem T000248

¬ ⇒