let M be PseudoMetricSpace; :: thesis: for VQ being Element of [:(M -neighbour),(M -neighbour):] holds
( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
let VQ be Element of [:(M -neighbour),(M -neighbour):]; :: thesis: ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )
( VQ in elem_in_rel M implies ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) )

proof

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

end;

hence ( VQ in elem_in_rel M iff ex V, Q being Element of M -neighbour ex v being Element of REAL st
( VQ = [V,Q] & V,Q is_dst v ) ) ; :: thesis: verum