A4: ].0 ,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:46;
A5: 0 in ].(- (PI / 2)),(PI / 2).[ ;
{0 } c= ].(- (PI / 2)),(PI / 2).[

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {0 } or x in ].(- (PI / 2)),(PI / 2).[ )
assume x in {0 } ; :: thesis: x in ].(- (PI / 2)),(PI / 2).[
hence x in ].(- (PI / 2)),(PI / 2).[ by A5, TARSKI:def 1; :: thesis: verum

end;

then ].0 ,(PI / 2).[ \/ {0 } c= ].(- (PI / 2)),(PI / 2).[ by A4, XBOOLE_1:8;
hence [.0 ,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ by XXREAL_1:131; :: thesis: verum