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

proof

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

end;

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