[.0 ,(PI / 4).] c= [.0 ,(PI / 2).[ by Lm5, XXREAL_2:def 12;
then sec | [.0 ,(PI / 4).] is increasing by Th17, RFUNCT_2:60;
hence (sec | [.0 ,(PI / 4).]) | [.0 ,(PI / 4).] is increasing ; :: thesis: verum