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