set A = { f where f is continuous RealMap of X : verum } ;
{ f where f is continuous RealMap of X : verum } c= Funcs the carrier of X,REAL

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { f where f is continuous RealMap of X : verum } or x in Funcs the carrier of X,REAL )
assume x in { f where f is continuous RealMap of X : verum } ; :: thesis: x in Funcs the carrier of X,REAL
then ex f being continuous RealMap of X st x = f ;
hence x in Funcs the carrier of X,REAL by FUNCT_2:11; :: thesis: verum

end;

hence { f where f is continuous RealMap of X : verum } is Subset of (RAlgebra the carrier of X) ; :: thesis: verum