Theorem T000753