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