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