let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour
for v being Element of 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 Element of 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 Element of 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

assume A2: 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
A3: V = p -neighbour by Th23;
A4: p in V by A3, Th9;
consider q being Element of M such that
A5: Q = q -neighbour by Th23;
A6: q in Q by A5, Th9;
then dist p,q = v by A2, A4, Def5;
hence ex p, q being Element of M st
( p in V & q in Q & dist p,q = v ) by A3, A6, Th9; :: 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 )

proof

assume ex p, q being Element of M st
( p in V & q in Q & dist p,q = v ) ; :: thesis: V,Q is_dst v
then for p1, q1 being Element of M st p1 in V & q1 in Q holds
dist p1,q1 = v by Th29;
hence V,Q is_dst v by Def5; :: thesis: verum

end;

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