let Omega be non empty set ; :: thesis: for F being SigmaField of Omega
for x being object holds
( x in set_of_random_variables_on (F,Borel_Sets) iff x is random_variable of F, Borel_Sets )
let F be SigmaField of Omega; :: thesis: for x being object holds
( x in set_of_random_variables_on (F,Borel_Sets) iff x is random_variable of F, Borel_Sets )
let x be object ; :: thesis: ( x in set_of_random_variables_on (F,Borel_Sets) iff x is random_variable of F, Borel_Sets )
thus ( x in set_of_random_variables_on (F,Borel_Sets) implies x is random_variable of F, Borel_Sets ) :: thesis: ( x is random_variable of F, Borel_Sets implies x in set_of_random_variables_on (F,Borel_Sets) )

proof

assume x in set_of_random_variables_on (F,Borel_Sets) ; :: thesis: x is random_variable of F, Borel_Sets
then consider M being Function of Omega,REAL such that
AA: ( x = M & M is F, Borel_Sets -random_variable-like ) ;
thus x is random_variable of F, Borel_Sets by AA; :: thesis: verum

end;

thus ( x is random_variable of F, Borel_Sets implies x in set_of_random_variables_on (F,Borel_Sets) ) ; :: thesis: verum