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.[ by A2, TARSKI:def 1;
].(- (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