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