:: deftheorem Def2 defines Real-Valued-Random-Variable RANDOM_1:def 2 :
for Omega being non empty set
for Sigma being SigmaField of Omega
for b₃ being Function of Omega,REAL holds
( b₃ is Real-Valued-Random-Variable of Sigma iff b₃ is [#] Sigma -measurable );