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

proof

let x be object ; :: thesis: ( x in set_of_constant_RV F implies x is random_variable of F, Borel_Sets )
assume x in set_of_constant_RV F ; :: thesis: x is random_variable of F, Borel_Sets
then consider f being Function of Omega,REAL such that
A1: ( x = f & f is random_variable of F, Borel_Sets & f is constant ) ;
thus x is random_variable of F, Borel_Sets by A1; :: thesis: verum

end;

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