PI in ].0,4.[ by SIN_COS:def 28;
then PI > 0 by XXREAL_1:4;
then A1: PI / 2 > 0 / 2 by XREAL_1:74;
0 - (PI / 2) < 0 by XREAL_1:49;
then A2: 0 in ].(- (PI / 2)),(PI / 2).[ by A1, XXREAL_1:4;
then tan . 0 = 0 / (cos . 0) by Th1, RFUNCT_1:def 1, SIN_COS:30
.= 0 ;
hence ( tan . 0 = 0 & tan 0 = 0 ) by A2, Th13; :: thesis: verum