consider Y being Subset of REAL such that
A2: Y = NAT by NUMBERS:19;
Y ` is Event of Borel_Sets by ZV5, A2, PROB_1:20;
hence REAL \ NAT is Event of Borel_Sets by A2; :: thesis: verum