Theorem T000808