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

proof

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

end;

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