Theorem T000685

⇒ ¬