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] & V,Q is_dst v ) by Th46;
A2: V in elem_in_rel_1 M by A1;
A3: Q in elem_in_rel_2 M by A1;
v in real_in_rel M by A1;
hence VQv in [:(elem_in_rel_1 M),(elem_in_rel_2 M),(real_in_rel M):] by A1, A2, 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