let M be PseudoMetricSpace; 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:];
( 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
;
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 Th29;
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:69;
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:2; verum