A1: (3 / 4) * PI < PI by XREAL_1:157;
thus (3 / 4) * PI in ].0,PI.[ by A1, XXREAL_1:4; :: thesis: verum