set z = the Element of X;

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

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

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

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

end;

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

end;

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