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