Theorem T000497