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