A1:
0 in ].(- (PI / 2)),(PI / 2).[
;
A2:
{0} c= ].(- (PI / 2)),(PI / 2).[
by A1, TARSKI:def 1;
].0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[
by XXREAL_1:46;
then
].0,(PI / 2).[ \/ {0} c= ].(- (PI / 2)),(PI / 2).[
by A2, XBOOLE_1:8;
hence
[.0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[
by XXREAL_1:131; verum