let M be PseudoMetricSpace; for v being Element of REAL
for W being Element of [:(M -neighbour),(M -neighbour):] holds
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
let v be Element of REAL ; for W being Element of [:(M -neighbour),(M -neighbour):] holds
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
let W be Element of [:(M -neighbour),(M -neighbour):]; ( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
( W in ev_eq_2 (v,M) implies ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
proof
assume
W in ev_eq_2 (
v,
M)
;
ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v )
then
ex
S being
Element of
[:(M -neighbour),(M -neighbour):] st
(
W = S & ex
V,
Q being
Element of
M -neighbour st
(
S = [V,Q] &
V,
Q is_dst v ) )
;
hence
ex
V,
Q being
Element of
M -neighbour st
(
W = [V,Q] &
V,
Q is_dst v )
;
verum
end;
hence
( W in ev_eq_2 (v,M) iff ex V, Q being Element of M -neighbour st
( W = [V,Q] & V,Q is_dst v ) )
; verum