defpred S₁[ 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 S₁[V,Q,v]

proof

let V, Q be Element of M -neighbour ; :: thesis: ex v being Element of REAL st S₁[V,Q,v]
consider v being Real such that
A2: S₁[V,Q,v] by Th33;
reconsider v = v as Element of REAL by XREAL_0:def 1;
take v ; :: thesis: S₁[V,Q,v]
thus S₁[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 S₁[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