PI in ].0 ,4.[ by SIN_COS:def 32;
hence not PI is negative by XXREAL_1:4; :: thesis: verum