set h = sec | ].(PI / 2),PI .];
X: [.((3 / 4) * PI ),PI .] c= ].(PI / 2),PI .] by Lm10, XXREAL_2:def 12;
then (sec | [.((3 / 4) * PI ),PI .]) " = ((sec | ].(PI / 2),PI .]) | [.((3 / 4) * PI ),PI .]) " by RELAT_1:103
.= ((sec | ].(PI / 2),PI .]) " ) | ((sec | ].(PI / 2),PI .]) .: [.((3 / 4) * PI ),PI .]) by RFUNCT_2:40
.= ((sec | ].(PI / 2),PI .]) " ) | (rng ((sec | ].(PI / 2),PI .]) | [.((3 / 4) * PI ),PI .])) by RELAT_1:148
.= ((sec | ].(PI / 2),PI .]) " ) | [.(- (sqrt 2)),(- 1).] by Th42, X, RELAT_1:103 ;
hence arcsec2 | [.(- (sqrt 2)),(- 1).] = (sec | [.((3 / 4) * PI ),PI .]) " ; :: thesis: verum