reconsider A = {1} as Subset of REAL ;
W1: A in Borel_Sets by Th1;
A ` in Borel_Sets by Th1, PROB_1:15;
then A \/ (A `) in Borel_Sets by W1, PROB_1:3;
then [#] REAL in Borel_Sets by SUBSET_1:10;
hence REAL is Event of Borel_Sets ; :: thesis: verum