theorem :: FINANCE5:4

for r being Real st r >= 0 holds
[.0,+infty.] \ [.0,r.[ = [.r,+infty.]