A1: [.(- 1),1.] = tan .: [.(- (PI / 4)),(PI / 4).] by Th21, RELAT_1:148;
[.(- (PI / 4)),(PI / 4).] c= ].(- (PI / 2)),(PI / 2).[ by Lm7, Lm8, XXREAL_2:def 12;
hence arctan | [.(- 1),1.] is increasing by A1, Th45, RELAT_1:156, RFUNCT_2:60; :: thesis: verum