let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour
for v being Real holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
let V, Q be Element of M -neighbour ; :: thesis: for v being Real holds
( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
let v be Real; :: thesis: ( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )
A1: ( V,Q is_dst v implies ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) )

proof

consider q being Element of M such that
A2: Q = q -neighbour by Th15;
A3: q in Q by A2, Th4;
assume A4: V,Q is_dst v ; :: thesis: ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v )
consider p being Element of M such that
A5: V = p -neighbour by Th15;
p in V by A5, Th4;
then dist (p,q) = v by A4, A3;
hence ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) by A5, A3, Th4; :: thesis: verum

end;

( ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) implies V,Q is_dst v ) by Th20;
hence ( V,Q is_dst v iff ex p, q being Element of M st
( p in V & q in Q & dist (p,q) = v ) ) by A1; :: thesis: verum