let Y be set ; :: thesis: for k being Nat st Y = REAL \ {k} holds
Y is Event of Borel_Sets
let k be Nat; :: thesis: ( Y = REAL \ {k} implies Y is Event of Borel_Sets )
assume A1: Y = REAL \ {k} ; :: thesis: Y is Event of Borel_Sets
reconsider Exx = k as Element of REAL by ORDINAL1:def 12, NUMBERS:19;
reconsider Z = {Exx} as Subset of REAL ;
Z ` is Element of Borel_Sets by PROB_1:15, Th1;
hence Y is Event of Borel_Sets by A1; :: thesis: verum