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