0 in [.0,1.] by XXREAL_1:1;
then A1: tan . 0 = (sin . 0) * ((cos . 0) ") by Th69, RFUNCT_1:def 1
.= 0 by Th30 ;
1 in [.0,1.] by XXREAL_1:1;
then tan . 1 = (sin . 1) / (cos . 1) by Th69, RFUNCT_1:def 1;
hence ( tan . 0 = 0 & tan . 1 > 1 ) by A1, Th42, XREAL_1:187; :: thesis: verum