A1: PI / 2 < PI / 1 by XREAL_1:76;
A2: PI < (3 / 2) * PI by XREAL_1:155;
then A3: PI in ].(PI / 2),((3 / 2) * PI).[ by A1;
A4: {PI} c= ].(PI / 2),((3 / 2) * PI).[ by A3, TARSKI:def 1;
].(PI / 2),PI.[ c= ].(PI / 2),((3 / 2) * PI).[ by A2, XXREAL_1:46;
then ].(PI / 2),PI.[ \/ {PI} c= ].(PI / 2),((3 / 2) * PI).[ by A4, XBOOLE_1:8;
hence ].(PI / 2),PI.] c= ].(PI / 2),((3 / 2) * PI).[ by A1, XXREAL_1:132; :: thesis: verum