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

proof

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

end;

hence ( v in real_in_rel M iff ex V, Q being Element of M -neighbour st V,Q is_dst v ) ; :: thesis: verum