Theorem T000513