set z = the Element of X;

A1: now :: thesis: for z being object st z in { |.(f . x).| where x is Element of X : verum } holds
z in REAL

let z be object ; :: thesis: ( z in { |.(f . x).| where x is Element of X : verum } implies z in REAL )

now :: thesis: ( z in { |.(f . x).| where x is Element of X : verum } implies z in REAL )

assume z in { |.(f . x).| where x is Element of X : verum } ; :: thesis: z in REAL
then ex x being Element of X st z = |.(f . x).| ;
hence z in REAL by XREAL_0:def 1; :: thesis: verum

end;

hence ( z in { |.(f . x).| where x is Element of X : verum } implies z in REAL ) ; :: thesis: verum

end;

|.(f . the Element of X).| in { |.(f . x).| where x is Element of X : verum } ;
hence { |.(f . x).| where x is Element of X : verum } is non empty Subset of REAL by A1, TARSKI:def 3; :: thesis: verum