PI in ].0 ,4.[ by SIN_COS:def 32;
then A1: PI > 0 by XXREAL_1:4;
then A2: PI / 4 < PI / 1 by XREAL_1:78;
PI / 4 > 0 / 4 by A1, XREAL_1:76;
hence PI / 4 in ].0 ,PI .[ by A2, XXREAL_1:4; :: thesis: verum