theorem Th9: :: FINANCE1:9

for Omega being non empty set
for Sigma being SigmaField of Omega
for X being Function of Omega,REAL st X is Sigma, Borel_Sets -random_variable-like holds
( ( for k being Real holds
( { w where w is Element of Omega : X . w >= k } is Element of Sigma & { w where w is Element of Omega : X . w < k } is Element of Sigma ) ) & ( for k1, k2 being Real st k1 < k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w < k2 ) } is Element of Sigma ) & ( for k1, k2 being Real st k1 <= k2 holds
{ w where w is Element of Omega : ( k1 <= X . w & X . w <= k2 ) } is Element of Sigma ) & ( for r being Real holds less_dom (X,r) = { w where w is Element of Omega : X . w < r } ) & ( for r being Real holds great_eq_dom (X,r) = { w where w is Element of Omega : X . w >= r } ) & ( for r being Real holds eq_dom (X,r) = { w where w is Element of Omega : X . w = r } ) & ( for r being Real holds eq_dom (X,r) is Element of Sigma ) )