let M be PseudoMetricSpace; for V, Q being Element of M -neighbour
for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
let V, Q be Element of M -neighbour ; for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
let v be Element of REAL ; ( V,Q is_dst v implies Q,V is_dst v )
assume
V,Q is_dst v
; Q,V is_dst v
then
for q, p being Element of M st q in Q & p in V holds
dist (q,p) = v
;
hence
Q,V is_dst v
; verum