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