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