A1: not { f where f is Real-Valued-Random-Variable of Sigma : verum } is empty

proof

consider g being Real-Valued-Random-Variable of Sigma;
g in { f where f is Real-Valued-Random-Variable of Sigma : verum } ;
hence not { f where f is Real-Valued-Random-Variable of Sigma : verum } is empty ; :: thesis: verum

end;

{ f where f is Real-Valued-Random-Variable of Sigma : verum } c= Funcs (Omega,REAL)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is Real-Valued-Random-Variable of Sigma : verum } or x in Funcs (Omega,REAL) )
assume x in { f where f is Real-Valued-Random-Variable of Sigma : verum } ; :: thesis: x in Funcs (Omega,REAL)
then consider f being Real-Valued-Random-Variable of Sigma such that
A2: x = f ;
thus x in Funcs (Omega,REAL) by FUNCT_2:11, A2; :: thesis: verum

end;

hence { f where f is Real-Valued-Random-Variable of Sigma : verum } is non empty Subset of (RAlgebra Omega) by A1; :: thesis: verum