set f = sec | ].(PI / 2),PI .];
A1: (sec | ].(PI / 2),PI .]) .: ].(PI / 2),PI .] = rng ((sec | ].(PI / 2),PI .]) | ].(PI / 2),PI .]) by RELAT_1:148
.= rng (sec | ].(PI / 2),PI .]) by RELAT_1:102
.= sec .: ].(PI / 2),PI .] by RELAT_1:148 ;
(sec | ].(PI / 2),PI .]) | ].(PI / 2),PI .] = sec | ].(PI / 2),PI .] by RELAT_1:102;
hence arcsec2 | (sec .: ].(PI / 2),PI .]) is increasing by A1, Th18, FCONT_3:17; :: thesis: verum