reconsider MyOmega = Omega as Element of F by PROB_1:5;
set g2 = chi (Omega,Omega);
chi (Omega,Omega) is random_variable of F, Borel_Sets by ChiRandom;
then chi (MyOmega,MyOmega) in set_of_chi_RV F ;
hence not set_of_chi_RV F is empty ; :: thesis: verum