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; verum