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

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

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

end;

assume ASS0: x in Bor2 \ Bor3 ; :: thesis:
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:

end;

end;