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:115
.= rng (sec | ].(PI / 2),PI.]) by RELAT_1:73
.= sec .: ].(PI / 2),PI.] by RELAT_1:115 ;
(sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.] = sec | ].(PI / 2),PI.] by RELAT_1:73;
hence arcsec2 | (sec .: ].(PI / 2),PI.]) is increasing by A1, Th18, FCONT_3:9; :: thesis: verum