let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v
let V, Q be Element of M -neighbour ; :: thesis: ex v being Element of REAL st V,Q is_dst v
consider p being Element of M such that
A1: V = p -neighbour by Th23;
A2: p in V by A1, Th9;
consider q being Element of M such that
A3: Q = q -neighbour by Th23;
q in Q by A3, Th9;
then V,Q is_dst dist p,q by A2, Th31;
hence ex v being Element of REAL st V,Q is_dst v ; :: thesis: verum