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; verum