let r be real number ; :: thesis: cos r <= 1
cos . r in [.(- 1),1.] by COMPTRIG:45;
then cos r in [.(- 1),1.] by SIN_COS:def 23;
hence cos r <= 1 by XXREAL_1:1; :: thesis: verum