[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0 .[ by Lm11, XXREAL_2:def 12;
then (cosec | [.(- (PI / 2)),0 .[) | [.(- (PI / 2)),(- (PI / 4)).] = cosec | [.(- (PI / 2)),(- (PI / 4)).] by RELAT_1:103;
hence cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one ; :: thesis: verum