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