defpred S1[ Element of M -neighbour , Element of M -neighbour , Real] means $1,$2 is_dst $3;
A1: for V, Q being Element of M -neighbour ex v being Element of REAL st S1[V,Q,v]
proof
let V, Q be Element of M -neighbour ; :: thesis: ex v being Element of REAL st S1[V,Q,v]
consider v being Real such that
A2: S1[V,Q,v] by Th33;
reconsider v = v as Element of REAL by XREAL_0:def 1;
take v ; :: thesis: S1[V,Q,v]
thus S1[V,Q,v] by A2; :: thesis: verum
end;
consider F being Function of [:(M -neighbour),(M -neighbour):],REAL such that
A3: for V, Q being Element of M -neighbour holds S1[V,Q,F . (V,Q)] from BINOP_1:sch 3(A1);
 take F ; :: thesis: for V, Q being Element of M -neighbour
for p, q being Element of M st p in V & q in Q holds
F . (V,Q) = dist (p,q)
let V, Q be Element of M -neighbour ; :: thesis: for p, q being Element of M st p in V & q in Q holds
F . (V,Q) = dist (p,q)
let p, q be Element of M; :: thesis: ( p in V & q in Q implies F . (V,Q) = dist (p,q) )
assume A4: ( p in V & q in Q ) ; :: thesis: F . (V,Q) = dist (p,q)
V,Q is_dst F . (V,Q) by A3;
hence F . (V,Q) = dist (p,q) by A4; :: thesis: verum