Theorem T000638

⇒ ¬