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;
consider q being Element of M such that
A2: Q = q -neighbour by Th23;
A3: q in Q by A2, Th9;
p in V by A1, Th9;
then V,Q is_dst dist (p,q) by A3, Th31;
hence ex v being Element of REAL st V,Q is_dst v ; :: thesis: verum