PI / 4 < PI / 2 by XREAL_1:76;
then - (PI / 4) > - (PI / 2) by XREAL_1:24;
hence ( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ ) ; :: thesis: verum