for Omega being non empty set
for Sigma being SigmaField of Omega
for f being Function of Omega,REAL holds
( f is random_variable of Sigma, Borel_Sets iff f is Real-Valued-Random-Variable of Sigma ) by Th7;