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

z in REAL

set z = the Element of X;z in REAL

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

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

hence
( z in { |.(f . x).| where x is Element of X : verum } implies z in REAL )
; :: thesis: verumassume
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;then ex x being Element of X st z = |.(f . x).| ;

hence z in REAL by XREAL_0:def 1; :: thesis: verum

|.(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