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