:: deftheorem defines Real-Valued-Random-Variables-Set RANDOM_2:def 3 :
for Omega being non empty set
for Sigma being SigmaField of Omega holds Real-Valued-Random-Variables-Set Sigma = { f where f is Real-Valued-Random-Variable of Sigma : verum } ;