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

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

suppose A2: x in ].0,(PI / 4).[ ; :: thesis: sec . x in [.1,(sqrt 2).]

PI / 4 < PI / 2 by XREAL_1:76;
then ( 0 in [.0,(PI / 2).[ & PI / 4 in [.0,(PI / 2).[ ) ;
then A3: [.0,(PI / 4).] c= [.0,(PI / 2).[ by XXREAL_2:def 12;
then A4: sec | [.0,(PI / 4).] is increasing by Th17, RFUNCT_2:28;
A5: ex s being Real st
( s = x & 0 < s & s < PI / 4 ) by A2;
A6: ].0,(PI / 4).[ c= [.0,(PI / 4).] by XXREAL_1:25;
A7: [.0,(PI / 4).] /\ (dom sec) = [.0,(PI / 4).] by A3, Th1, XBOOLE_1:1, XBOOLE_1:28;
( 0 in [.0,(PI / 4).] & ex s being Real st
( s = x & 0 < s & s < PI / 4 ) ) by A2;
then A8: 1 < sec . x by A2, A4, A7, A6, Th31, RFUNCT_2:20;
PI / 4 in [.0,(PI / 4).] /\ (dom sec) by A7;
then sec . x < sqrt 2 by A2, A4, A7, A6, A5, Th31, RFUNCT_2:20;
hence sec . x in [.1,(sqrt 2).] by A8; :: thesis: verum

end;

suppose x = 0 ; :: thesis: sec . x in [.1,(sqrt 2).]

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

end;

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

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

end;

end;