Theorem T000503