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

proof

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

end;

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