set Bor1 = ].0,+infty.[;
reconsider Bor3 = {0} as Event of Borel_Sets by FINANCE2:5;
reconsider Bor2 = [.0,+infty.[ as Event of Borel_Sets by FINANCE1:3;
].0,+infty.[ = Bor2 \ Bor3

proof

for x being object holds
( x in ].0,+infty.[ iff x in Bor2 \ Bor3 )

proof

let x be object ; :: thesis: ( x in ].0,+infty.[ iff x in Bor2 \ Bor3 )
thus ( x in ].0,+infty.[ implies x in Bor2 \ Bor3 ) :: thesis: ( x in Bor2 \ Bor3 implies x in ].0,+infty.[ )

proof

assume ASS0: x in ].0,+infty.[ ; :: thesis: x in Bor2 \ Bor3
then reconsider x = x as Real ;
d1: ( 0 < x & x < +infty ) by ASS0, XXREAL_1:4;
then D2: x in [.0,+infty.[ by XXREAL_1:3;
not x in {0} by d1, TARSKI:def 1;
hence x in Bor2 \ Bor3 by XBOOLE_0:def 5, D2; :: thesis: verum

end;

assume ASS0: x in Bor2 \ Bor3 ; :: thesis: x in ].0,+infty.[
then reconsider x = x as Real ;
( x in Bor2 & not x in Bor3 ) by ASS0, XBOOLE_0:def 5;
then ( 0 <= x & x < +infty & x <> 0 ) by TARSKI:def 1, XXREAL_1:3;
hence x in ].0,+infty.[ by XXREAL_1:4; :: thesis: verum

end;

hence ].0,+infty.[ = Bor2 \ Bor3 by TARSKI:2; :: thesis: verum

end;

hence ].0,+infty.[ is Element of Borel_Sets ; :: thesis: verum