set myRV = Omega --> 0;
A2: 0 in REAL by NUMBERS:19;
reconsider myRV = Omega --> 0 as Function of Omega,REAL by FUNCOP_1:45, NUMBERS:19;
myRV is F, Borel_Sets -random_variable-like by FINANCE3:10, A2;
then myRV in set_of_constant_RV F ;
hence not set_of_constant_RV F is empty ; :: thesis: verum