:: deftheorem Def555 defines TheEvent FINANCE5:def 4 :
for r being Real
for b₂ being Subset of REAL holds
( ( r <= 0 implies ( b₂ is TheEvent of r iff b₂ = [.0,+infty.[ ) ) & ( not r <= 0 implies ( b₂ is TheEvent of r iff b₂ = [.0,r.] ) ) );