[#] REAL in Borel_Sets by PROB_1:5;
hence P . REAL = 1 by Lm1; :: thesis: verum