( [.1,(sqrt 2).] = sec .: [.0 ,(PI / 4).] & [.0 ,(PI / 4).] c= [.0 ,(PI / 2).[ ) by Lm5, Th41, RELAT_1:148, XXREAL_2:def 12;
hence arcsec1 | [.1,(sqrt 2).] is increasing by Th77, RELAT_1:156, RFUNCT_2:60; :: thesis: verum