Theorem T000532