:: 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 ex X being Element of Sigma st
( X = Omega & b₃ is_measurable_on X ) );