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