0 in [.0 ,1.] by XXREAL_1:1;
then A2: tan . 0 = (sin . 0 ) * ((cos . 0 ) " ) by Th75, RFUNCT_1:def 4
.= 0 by Th33 ;
1 in [.0 ,1.] by XXREAL_1:1;
then tan . 1 = (sin . 1) / (cos . 1) by Th75, RFUNCT_1:def 4;
hence ( tan . 0 = 0 & tan . 1 > 1 ) by A2, Th47, XREAL_1:189; :: thesis: verum