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