defpred S1[ Element of M, Element of R^1] means for s being Element of M
for t being Element of R^1 st $1 = s & $2 = t holds
t = lower_bound ((dist s) .: P);
A7: for s being Element of M ex t being Element of R^1 st S1[s,t]
proof
let s be Element of M; :: thesis: ex t being Element of R^1 st S1[s,t]
set t = lower_bound ((dist s) .: P);
lower_bound ((dist s) .: P) in REAL by XREAL_0:def 1;
then reconsider t = lower_bound ((dist s) .: P) as Element of R^1 by TOPMETR:17;
take t ; :: thesis: S1[s,t]
thus S1[s,t] ; :: thesis: verum
end;
consider F being Function of the carrier of M, the carrier of R^1 such that
A8: for x being Element of M holds S1[x,F . x] from FUNCT_2:sch 3(A7);
 A9: for y being Point of M holds F . y = lower_bound ((dist y) .: P) by A8;
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
then reconsider F = F as Function of (TopSpaceMetr M),R^1 ;
take F ; :: thesis: for x being Point of M holds F . x = lower_bound ((dist x) .: P)
thus for x being Point of M holds F . x = lower_bound ((dist x) .: P) by A9; :: thesis: verum