A1: [.(- (sqrt 2)),(- 1).] = sec .: [.((3 / 4) * PI ),PI .] by Th42, RELAT_1:148;
[.((3 / 4) * PI ),PI .] c= ].(PI / 2),PI .] by Lm10, XXREAL_2:def 12;
then [.(- (sqrt 2)),(- 1).] c= sec .: ].(PI / 2),PI .] by A1, RELAT_1:156;
hence arcsec2 | [.(- (sqrt 2)),(- 1).] is increasing by Th78, RFUNCT_2:60; :: thesis: verum