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;