let M be PseudoMetricSpace; 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 ; 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 ; ( 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 )
hence
( v in ev_eq_1 (V,Q) iff V,Q is_dst v )
; verum