PI / 4 < PI / 2 by XREAL_1:76;
then ( (PI / 4) + (PI / 2) > 0 + (PI / 2) & (PI / 4) + (PI / 2) < (PI / 2) + (PI / 2) ) by XREAL_1:8;
hence ( (3 / 4) * PI in ].(PI / 2),PI.] & PI in ].(PI / 2),PI.] ) by COMPTRIG:5; :: thesis: verum