X: ].(- (PI / 2)),(PI / 2).[ c= dom tan by Th1;
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 A2: x0 in ].(- (PI / 2)),(PI / 2).[ ; :: thesis: 0 < diff tan ,x0
0 < cos . x0 by A2, COMPTRIG:27;
then A4: (cos . x0) ^2 > 0 by SQUARE_1:74;
1 / ((cos . x0) ^2 ) > 0 / ((cos . x0) ^2 ) by A4, XREAL_1:76;
hence 0 < diff tan ,x0 by A2, Lm3; :: thesis: verum

end;

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