for x being object st x in set_of_chi_RV F holds
x is random_variable of F, Borel_Sets

proof

let x be object ; :: thesis: ( x in set_of_chi_RV F implies x is random_variable of F, Borel_Sets )
assume x in set_of_chi_RV F ; :: thesis: x is random_variable of F, Borel_Sets
then consider A being Element of F such that
A1: ( x = chi (A,Omega) & chi (A,Omega) is random_variable of F, Borel_Sets ) ;
thus x is random_variable of F, Borel_Sets by A1; :: thesis: verum

end;

hence set_of_chi_RV F is F -random-membered ; :: thesis: verum