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).[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {PI} or x in ].(PI / 2),((3 / 2) * PI).[ )
assume x in {PI} ; :: thesis: x in ].(PI / 2),((3 / 2) * PI).[
hence x in ].(PI / 2),((3 / 2) * PI).[ by A3, TARSKI:def 1; :: thesis: verum

end;

].(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