A1: PI / 4 < PI / 1 by XREAL_1:76;
thus PI / 4 in ].0,PI.[ by A1, XXREAL_1:4; :: thesis: verum