A2: (PI / 4) + (PI / 2) > 0 + (PI / 2) by XREAL_1:10;
PI / 4 < PI / 2 by XREAL_1:78;
then (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 A2, COMPTRIG:21; :: thesis: verum