Theorem T000628