let x be set ; :: thesis: ( x in [.(PI / 4),(PI / 2).] implies cosec . x in [.1,(sqrt 2).] )
A1: PI / 4 < PI / 2 by XREAL_1:76;
assume x in [.(PI / 4),(PI / 2).] ; :: thesis: cosec . x in [.1,(sqrt 2).]
then x in ].(PI / 4),(PI / 2).[ \/ {(PI / 4),(PI / 2)} by A1, XXREAL_1:128;
then A2: ( x in ].(PI / 4),(PI / 2).[ or x in {(PI / 4),(PI / 2)} ) by XBOOLE_0:def 3;

per cases ( x in ].(PI / 4),(PI / 2).[ or x = PI / 4 or x = PI / 2 ) by A2, TARSKI:def 2;

suppose A3: x in ].(PI / 4),(PI / 2).[ ; :: thesis: cosec . x in [.1,(sqrt 2).]

then A4: ex s being Real st
( s = x & PI / 4 < s & s < PI / 2 ) ;
A5: ex s being Real st
( s = x & PI / 4 < s & s < PI / 2 ) by A3;
A6: ].(PI / 4),(PI / 2).[ c= [.(PI / 4),(PI / 2).] by XXREAL_1:25;
( PI / 4 in ].0,(PI / 2).] & PI / 2 in ].0,(PI / 2).] ) by A1;
then A7: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by XXREAL_2:def 12;
then A8: cosec | [.(PI / 4),(PI / 2).] is decreasing by Th20, RFUNCT_2:29;
A9: [.(PI / 4),(PI / 2).] /\ (dom cosec) = [.(PI / 4),(PI / 2).] by A7, Th4, XBOOLE_1:1, XBOOLE_1:28;
then PI / 2 in [.(PI / 4),(PI / 2).] /\ (dom cosec) by A1;
then A10: cosec . x > 1 by A3, A8, A9, A6, A5, Th32, RFUNCT_2:21;
PI / 4 in [.(PI / 4),(PI / 2).] by A1;
then sqrt 2 > cosec . x by A3, A8, A9, A6, A4, Th32, RFUNCT_2:21;
hence cosec . x in [.1,(sqrt 2).] by A10; :: thesis: verum

end;

suppose x = PI / 4 ; :: thesis: cosec . x in [.1,(sqrt 2).]

hence cosec . x in [.1,(sqrt 2).] by Th32, SQUARE_1:19; :: thesis: verum

end;

suppose x = PI / 2 ; :: thesis: cosec . x in [.1,(sqrt 2).]

hence cosec . x in [.1,(sqrt 2).] by Th32, SQUARE_1:19; :: thesis: verum

end;

end;