A2: PI / 2 < PI / 1 by XREAL_1:78;
then A3: ].0 ,(PI / 2).[ c= ].0 ,PI .[ by XXREAL_1:46;
A5: PI / 2 in ].0 ,PI .[ by A2, XXREAL_1:4;
{(PI / 2)} c= ].0 ,PI .[

proof

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

end;

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