let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour ex v being Real st V,Q is_dst v
let V, Q be Element of M -neighbour ; :: thesis: ex v being Real st V,Q is_dst v
consider p being Element of M such that
A1: V = p -neighbour by Th15;
consider q being Element of M such that
A2: Q = q -neighbour by Th15;
A3: q in Q by A2, Th4;
p in V by A1, Th4;
then V,Q is_dst dist (p,q) by A3, Th21;
hence ex v being Real st V,Q is_dst v ; :: thesis: verum