let M be PseudoMetricSpace; :: thesis: set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
for VQv being Element of [:(M -neighbour ),(M -neighbour ),REAL :] st VQv in set_in_rel M holds
VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]

proof

let VQv be Element of [:(M -neighbour ),(M -neighbour ),REAL :]; :: thesis: ( VQv in set_in_rel M implies VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] )
assume VQv in set_in_rel M ; :: thesis: VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):]
then consider V, Q being Element of M -neighbour , v being Element of REAL such that
A1: VQv = [V,Q,v] and
A2: V,Q is_dst v by Th46;
A3: v in real_in_rel M by A2;
( V in elem_in_rel_1 M & Q in elem_in_rel_2 M ) by A2;
hence VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by A1, A3, MCART_1:73; :: thesis: verum

end;

hence set_in_rel M c= [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by SUBSET_1:7; :: thesis: verum