let x be set ; ( x in [.1,(sqrt 2).] implies arccosec2 . x in [.(PI / 4),(PI / 2).] )
assume
x in [.1,(sqrt 2).]
; arccosec2 . x in [.(PI / 4),(PI / 2).]
then
x in ].1,(sqrt 2).[ \/ {1,(sqrt 2)}
by SQUARE_1:19, XXREAL_1:128;
then A1:
( x in ].1,(sqrt 2).[ or x in {1,(sqrt 2)} )
by XBOOLE_0:def 3;
per cases
( x in ].1,(sqrt 2).[ or x = 1 or x = sqrt 2 )
by A1, TARSKI:def 2;
suppose A2:
x in ].1,(sqrt 2).[
;
arccosec2 . x in [.(PI / 4),(PI / 2).]then A3:
(
].1,(sqrt 2).[ c= [.1,(sqrt 2).] & ex
s being
Real st
(
s = x & 1
< s &
s < sqrt 2 ) )
by XXREAL_1:25;
A4:
[.1,(sqrt 2).] /\ (dom arccosec2) = [.1,(sqrt 2).]
by Th48, XBOOLE_1:28;
then
sqrt 2
in [.1,(sqrt 2).] /\ (dom arccosec2)
by SQUARE_1:19;
then A5:
arccosec2 . x > PI / 4
by A2, A4, A3, Th76, Th84, RFUNCT_2:21;
1
in [.1,(sqrt 2).]
by SQUARE_1:19;
then
PI / 2
> arccosec2 . x
by A2, A4, A3, Th76, Th84, RFUNCT_2:21;
hence
arccosec2 . x in [.(PI / 4),(PI / 2).]
by A5;
verum end; end;