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