A1: [.(- (sqrt 2)),(- 1).] = cosec .: [.(- (PI / 2)),(- (PI / 4)).] by Th43, RELAT_1:148;
[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[ by Lm11, XXREAL_2:def 12;
then [.(- (sqrt 2)),(- 1).] c= cosec .: [.(- (PI / 2)),0 .[ by A1, RELAT_1:156;
hence arccosec1 | [.(- (sqrt 2)),(- 1).] is decreasing by Th79, RFUNCT_2:61; :: thesis: verum