let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour
for v being Element of REAL holds
( v in ev_eq_1 V,Q iff V,Q is_dst v )
let V, Q be Element of M -neighbour ; :: thesis: for v being Element of REAL holds
( v in ev_eq_1 V,Q iff V,Q is_dst v )
let v be Element of REAL ; :: thesis: ( v in ev_eq_1 V,Q iff V,Q is_dst v )
( v in ev_eq_1 V,Q implies V,Q is_dst v )

proof

assume v in ev_eq_1 V,Q ; :: thesis: V,Q is_dst v
then ex r being Element of REAL st
( r = v & V,Q is_dst r ) ;
hence V,Q is_dst v ; :: thesis: verum

end;

hence ( v in ev_eq_1 V,Q iff V,Q is_dst v ) ; :: thesis: verum