PI / 2 < PI / 1 by XREAL_1:76;
then A1: - PI < - (PI / 2) by XREAL_1:24;
then A2: - (PI / 2) in ].(- PI),0.[ ;
A3: {(- (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 A2, TARSKI:def 1; :: thesis: verum

end;

].(- (PI / 2)),0.[ c= ].(- PI),0.[ by A1, XXREAL_1:46;
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