A1: now

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

now

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 ; :: thesis: verum

end;

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

end;

set z = the Element of X;
|.(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