( [.(- (sqrt 2)),(- 1).] = cosec .: [.(- (PI / 2)),(- (PI / 4)).] & [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ )
by Lm7, Th43, RELAT_1:115, XXREAL_2:def 12;
hence
arccosec1 | [.(- (sqrt 2)),(- 1).] is decreasing
by Th79, RELAT_1:123, RFUNCT_2:29; verum