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