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