let r be Real; :: thesis: for I being TheEvent of r holds I is Event of Borel_Sets
let I be TheEvent of r; :: thesis: I is Event of Borel_Sets
per cases ( r <= 0 or r > 0 ) ;
suppose S1: r <= 0 ; :: thesis: I is Event of Borel_Sets
[.0,+infty.[ is Element of Borel_Sets by FINANCE1:3;
hence I is Event of Borel_Sets by S1, Def555; :: thesis: verum
end;
suppose S1: r > 0 ; :: thesis: I is Event of Borel_Sets
[.0,r.] is Element of Borel_Sets by FINANCE1:8;
hence I is Event of Borel_Sets by S1, Def555; :: thesis: verum
end;
end;