A1: for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff (tan,x) > 0

proof

let x be Real; :: thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies diff (tan,x) > 0 )
assume A2: x in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: diff (tan,x) > 0
then 0 < cos . x by COMPTRIG:11;
then (cos . x) ^2 > 0 ;
then 1 / ((cos . x) ^2) > 0 / ((cos . x) ^2) ;
hence diff (tan,x) > 0 by A2, Lm3; :: thesis: verum

end;

].(- (PI / 2)),(PI / 2).[ c= dom tan by Lm1, FDIFF_1:def 6;
hence tan | ].(- (PI / 2)),(PI / 2).[ is increasing by A1, Lm1, ROLLE:9; :: thesis: verum