for x0 being Real st x0 in ].(- (PI / 2)),(PI / 2).[ holds
0 < diff (tan,x0)

proof

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

end;

then rng (tan | ].(- (PI / 2)),(PI / 2).[) is open by Lm1, Th1, FDIFF_2:41;
hence dom arctan is open by FUNCT_1:33; :: thesis: verum