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