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:27;
then (cos . x0) ^2 > 0 by SQUARE_1:74;
then 1 / ((cos . x0) ^2 ) > 0 / ((cos . x0) ^2 ) by XREAL_1:76;
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:55; :: thesis: verum