Theorem T000555

⇒ ¬