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