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