let M be PseudoMetricSpace; :: thesis: elem_in_rel_1 M = elem_in_rel_2 M
for V being Element of M -neighbour st V in elem_in_rel_2 M holds
V in elem_in_rel_1 M
proof
let V be Element of M -neighbour ; :: thesis: ( V in elem_in_rel_2 M implies V in elem_in_rel_1 M )
assume V in elem_in_rel_2 M ; :: thesis: V in elem_in_rel_1 M
then consider Q being Element of M -neighbour , v being Element of REAL such that
A1: Q,V is_dst v by Th27;
V,Q is_dst v by A1, Th22;
hence V in elem_in_rel_1 M ; :: thesis: verum
end;
then A2: elem_in_rel_2 M c= elem_in_rel_1 M by SUBSET_1:2;
for V being Element of M -neighbour st V in elem_in_rel_1 M holds
V in elem_in_rel_2 M
proof
let V be Element of M -neighbour ; :: thesis: ( V in elem_in_rel_1 M implies V in elem_in_rel_2 M )
assume V in elem_in_rel_1 M ; :: thesis: V in elem_in_rel_2 M
then consider Q being Element of M -neighbour , v being Element of REAL such that
A3: V,Q is_dst v by Th26;
Q,V is_dst v by A3, Th22;
hence V in elem_in_rel_2 M ; :: thesis: verum
end;
then elem_in_rel_1 M c= elem_in_rel_2 M by SUBSET_1:2;
hence elem_in_rel_1 M = elem_in_rel_2 M by A2, XBOOLE_0:def 10; :: thesis: verum