Theorem T000538