Theorem T000250

¬ ⇒