REAL c= REAL ;
then reconsider Omega = REAL as Subset of REAL ;
Omega in Borel_Sets by PROB_1:11;
hence P . REAL = 1 by Lm1; :: thesis: verum