set myRV = Omega --> 0;
0 in REAL by NUMBERS:19;
then ex K being Element of REAL st
( Omega --> 0 is_random_variable_on F, Borel_Sets & Omega --> 0 = Omega --> K ) by FINANCE3:10;
then Omega --> 0 in set_of_constant_RV F ;
hence not set_of_constant_RV F is empty ; :: thesis: verum