set f = cosec | [.(- (PI / 2)),(- (PI / 4)).];
- (PI / 2) <= - (PI / 4) by Lm7, XXREAL_1:3;
then ( (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] = cosec | [.(- (PI / 2)),(- (PI / 4)).] & (((cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).]) ") | ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) .: [.(- (PI / 2)),(- (PI / 4)).]) is continuous ) by Lm31, Lm39, FCONT_1:47, RELAT_1:72;
then (arccosec1 | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is continuous by Th43, Th51, RELAT_1:115;
hence arccosec1 | [.(- (sqrt 2)),(- 1).] is continuous by FCONT_1:15; :: thesis: verum