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