set f = cosec | ].0 ,(PI / 2).];
A1: (cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).] = cosec | ].0 ,(PI / 2).] by RELAT_1:102;
A2: (cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).] is decreasing by Th20;
(cosec | ].0 ,(PI / 2).]) .: ].0 ,(PI / 2).] = rng ((cosec | ].0 ,(PI / 2).]) | ].0 ,(PI / 2).]) by RELAT_1:148
.= rng (cosec | ].0 ,(PI / 2).]) by RELAT_1:102
.= cosec .: ].0 ,(PI / 2).] by RELAT_1:148 ;
hence arccosec2 | (cosec .: ].0 ,(PI / 2).]) is decreasing by A1, A2, FCONT_3:18; :: thesis: verum