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