for Omega being non empty set
for Sigma being SigmaField of Omega
for F being Function of Omega,REAL st F is Real-Valued-Random-Variable of Sigma holds
{ x where x is Element of Borel_Sets : F " x is Element of Sigma } is SigmaField of REAL