Theorem T000387