A1: PI / 2 < PI / 1 by XREAL_1:76;
then A2: PI / 2 in ].0,PI.[ ;
A3: {(PI / 2)} c= ].0,PI.[ by A2, TARSKI:def 1;
].0,(PI / 2).[ c= ].0,PI.[ by A1, XXREAL_1:46;
then ].0,(PI / 2).[ \/ {(PI / 2)} c= ].0,PI.[ by A3, XBOOLE_1:8;
hence ].0,(PI / 2).] c= ].0,PI.[ by XXREAL_1:132; :: thesis: verum