let Omega be non empty set ; :: thesis: for Sigma being SigmaField of Omega holds set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma
let Sigma be SigmaField of Omega; :: thesis: set_of_random_variables_on (Sigma,Borel_Sets) c= Real-Valued-Random-Variables-Set Sigma
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in set_of_random_variables_on (Sigma,Borel_Sets) or x in Real-Valued-Random-Variables-Set Sigma )
assume x in set_of_random_variables_on (Sigma,Borel_Sets) ; :: thesis: x in Real-Valued-Random-Variables-Set Sigma
then consider f being Function of Omega,REAL such that
J0: ( x = f & f is_random_variable_on Sigma, Borel_Sets ) ;
J1: ( f is_random_variable_on Sigma, Borel_Sets implies f is Real-Valued-Random-Variable of Sigma ) by Th10;
x in { q where q is Real-Valued-Random-Variable of Sigma : verum } by J1, J0;
hence x in Real-Valued-Random-Variables-Set Sigma by RANDOM_2:def 3; :: thesis: verum