let M be PseudoMetricSpace; :: thesis: 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 ; :: thesis: for v being Element of REAL st V,Q is_dst v holds
Q,V is_dst v
let v be Element of REAL ; :: thesis: ( V,Q is_dst v implies Q,V is_dst v )
assume V,Q is_dst v ; :: thesis: 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 ; :: thesis: verum