let M be PseudoMetricSpace; 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 ; 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; ( 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
;
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;
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; verum