A2: PI < (3 / 2) * PI by XREAL_1:157;
A3: ].(PI / 2),PI .[ c= ].(PI / 2),((3 / 2) * PI ).[ by A2, XXREAL_1:46;
A4: PI / 2 < PI / 1 by XREAL_1:78;
then A5: PI in ].(PI / 2),((3 / 2) * PI ).[ by A2;
{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 A5, TARSKI:def 1; :: thesis: verum

end;

then ].(PI / 2),PI .[ \/ {PI } c= ].(PI / 2),((3 / 2) * PI ).[ by A3, XBOOLE_1:8;
hence ].(PI / 2),PI .] c= ].(PI / 2),((3 / 2) * PI ).[ by A4, XXREAL_1:132; :: thesis: verum