PI in ].0 ,4.[ by SIN_COS:def 32;
then PI > 0 by XXREAL_1:4;
then A2: PI / 2 > 0 / 2 by XREAL_1:76;
0 - (PI / 2) < 0 by XREAL_1:51;
then A4: 0 in ].(- (PI / 2)),(PI / 2).[ by A2, XXREAL_1:4;
tan . 0 = 0 / (cos . 0 ) by A4, Th1, RFUNCT_1:def 4, SIN_COS:33
.= 0 ;
hence ( tan . 0 = 0 & tan 0 = 0 ) by A4, Th13; :: thesis: verum