PI in ].0 ,4.[ by SIN_COS:def 32;
hence PI > 0 by XXREAL_1:4; :: according to XXREAL_0:def 6 :: thesis: verum