Theorem T000739