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