let M be PseudoMetricSpace; :: thesis: 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 ; :: thesis: 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):]; :: thesis: ( 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) ; :: thesis: 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 ) ; :: thesis: 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 ) ) ; :: thesis: verum