A1: [.1,(sqrt 2).] = cosec .: [.(PI / 4),(PI / 2).] by Th44, RELAT_1:148;
[.(PI / 4),(PI / 2).] c= ].0 ,(PI / 2).] by Lm12, XXREAL_2:def 12;
then [.1,(sqrt 2).] c= cosec .: ].0 ,(PI / 2).] by A1, RELAT_1:156;
hence arccosec2 | [.1,(sqrt 2).] is decreasing by Th80, RFUNCT_2:61; :: thesis: verum