A1: 0 in REAL by XREAL_0:def 1;
[#] REAL in Borel_Sets by PROB_1:5;
hence P . REAL = 1 by Lm1, A1; :: thesis: verum