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