set f = cosec | [.(- (PI / 2)),0 .[;
A1: (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 ;
(cosec | [.(- (PI / 2)),0 .[) | [.(- (PI / 2)),0 .[ = cosec | [.(- (PI / 2)),0 .[ by RELAT_1:102;
hence arccosec1 | (cosec .: [.(- (PI / 2)),0 .[) is decreasing by A1, Th19, FCONT_3:18; :: thesis: verum