A1: PI / 2 < PI / 1 by XREAL_1:78;
A2: PI < (3 / 2) * PI by XREAL_1:157;
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