[.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def 12;
hence dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (PI / 2)),(- (PI / 4)).] by Th3, RELAT_1:62, XBOOLE_1:1; :: thesis: verum