theorem Th29: :: METRIC_2:29

for M being PseudoMetricSpace
for VQv being Element of [:(M -neighbour),(M -neighbour),REAL:] holds
( VQv in set_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQv = [V,Q,v] & V,Q is_dst v ) )