set f = cosec | [.(- (PI / 2)),0 .[;
A1: (cosec | [.(- (PI / 2)),0 .[) | [.(- (PI / 2)),0 .[ = cosec | [.(- (PI / 2)),0 .[ by RELAT_1:102;
A2: (cosec | [.(- (PI / 2)),0 .[) | [.(- (PI / 2)),0 .[ is decreasing by Th19;
(cosec | [.(- (PI / 2)),0 .[) .: [.(- (PI / 2)),0 .[ = rng ((cosec | [.(- (PI / 2)),0 .[) | [.(- (PI / 2)),0 .[) by RELAT_1:148
.= rng (cosec | [.(- (PI / 2)),0 .[) by RELAT_1:102
.= cosec .: [.(- (PI / 2)),0 .[ by RELAT_1:148 ;
hence arccosec1 | (cosec .: [.(- (PI / 2)),0 .[) is decreasing by A1, A2, FCONT_3:18; :: thesis: verum