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 object ; :: 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

A1: ( x = f & f is Sigma, Borel_Sets -random_variable-like ) ;

A2: ( f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma ) by Th15;

x in { q where q is Real-Valued-Random-Variable of Sigma : verum } by A2, A1;

hence x in Real-Valued-Random-Variables-Set Sigma by RANDOM_2:def 3; :: thesis: verum

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 object ; :: 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

A1: ( x = f & f is Sigma, Borel_Sets -random_variable-like ) ;

A2: ( f is Sigma, Borel_Sets -random_variable-like implies f is Real-Valued-Random-Variable of Sigma ) by Th15;

x in { q where q is Real-Valued-Random-Variable of Sigma : verum } by A2, A1;

hence x in Real-Valued-Random-Variables-Set Sigma by RANDOM_2:def 3; :: thesis: verum