let M be PseudoMetricSpace; :: thesis: for Q being Element of M -neighbour holds
( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
let Q be Element of M -neighbour ; :: thesis: ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
( Q in elem_in_rel_2 M implies ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v )
proof
assume Q in elem_in_rel_2 M ; :: thesis: ex V 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 = Q & ex V being Element of M -neighbour ex v being Element of REAL st V,S is_dst v ) ;
hence ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ; :: thesis: verum
end;
hence ( Q in elem_in_rel_2 M iff ex V being Element of M -neighbour ex v being Element of REAL st V,Q is_dst v ) ; :: thesis: verum