deffunc H₁( Element of X) -> Element of REAL = lower_bound ((dist f,$1) .: A);
consider INF being Function of X,REAL such that
A1: for x being Element of X holds INF . x = H₁(x) from FUNCT_2:sch 4();
take INF ; :: thesis: for x being Element of X holds INF . x = inf ((dist f,x) .: A)
thus for x being Element of X holds INF . x = inf ((dist f,x) .: A) by A1; :: thesis: verum