PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: PI > 0 by XXREAL_1:4;
then A2: (3 / 4) * PI > (3 / 4) * 0 by XREAL_1:70;
(3 / 4) * PI < PI by A1, XREAL_1:159;
hence (3 / 4) * PI in ].0 ,PI .[ by A2, XXREAL_1:4; :: thesis: verum