let x be set ; :: thesis: ( x in [.1,(sqrt 2).] implies arcsec1 . x in [.0,(PI / 4).] )
assume x in [.1,(sqrt 2).] ; :: thesis: arcsec1 . x in [.0,(PI / 4).]
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).[ ; :: thesis: arcsec1 . x in [.0,(PI / 4).]
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 arcsec1) = [.1,(sqrt 2).] by Th45, XBOOLE_1:28;
then sqrt 2 in [.1,(sqrt 2).] /\ (dom arcsec1) by SQUARE_1:19;
then A5: arcsec1 . x < PI / 4 by A2, A4, A3, Th73, Th81, RFUNCT_2:20;
1 in [.1,(sqrt 2).] by SQUARE_1:19;
then 0 < arcsec1 . x by A2, A4, A3, Th73, Th81, RFUNCT_2:20;
hence arcsec1 . x in [.0,(PI / 4).] by A5; :: thesis: verum
end;
suppose x = 1 ; :: thesis: arcsec1 . x in [.0,(PI / 4).]
hence arcsec1 . x in [.0,(PI / 4).] by Th73; :: thesis: verum
end;
suppose x = sqrt 2 ; :: thesis: arcsec1 . x in [.0,(PI / 4).]
hence arcsec1 . x in [.0,(PI / 4).] by Th73; :: thesis: verum
end;
end;