let r be Real; :: thesis: - 1 <= cos r
cos . r in [.(- 1),1.] by COMPTRIG:27;
then cos r in [.(- 1),1.] by SIN_COS:def 19;
hence - 1 <= cos r by XXREAL_1:1; :: thesis: verum