( [.(- (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; :: thesis: verum