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