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