set f = sec | [.0 ,(PI / 2).[;
A1: (sec | [.0 ,(PI / 2).[) | [.0 ,(PI / 2).[ = sec | [.0 ,(PI / 2).[ by RELAT_1:102;
A2: (sec | [.0 ,(PI / 2).[) | [.0 ,(PI / 2).[ is increasing by Th17;
(sec | [.0 ,(PI / 2).[) .: [.0 ,(PI / 2).[ = rng ((sec | [.0 ,(PI / 2).[) | [.0 ,(PI / 2).[) by RELAT_1:148
.= rng (sec | [.0 ,(PI / 2).[) by RELAT_1:102
.= sec .: [.0 ,(PI / 2).[ by RELAT_1:148 ;
hence arcsec1 | (sec .: [.0 ,(PI / 2).[) is increasing by A1, A2, FCONT_3:17; :: thesis: verum