for Y being set
for k being Nat st Y = REAL \ {k} holds
Y is Event of Borel_Sets