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