let M be PseudoMetricSpace; :: thesis: for V, Q being Element of M -neighbour
for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist p1,q1 = dist p2,q2
let V, Q be Element of M -neighbour ; :: thesis: for p1, p2, q1, q2 being Element of M st p1 in V & q1 in Q & p2 in V & q2 in Q holds
dist p1,q1 = dist p2,q2
let p1, p2, q1, q2 be Element of M; :: thesis: ( p1 in V & q1 in Q & p2 in V & q2 in Q implies dist p1,q1 = dist p2,q2 )
assume A1: ( p1 in V & q1 in Q & p2 in V & q2 in Q ) ; :: thesis: dist p1,q1 = dist p2,q2
V is equivalence_class of M by Th26;
then ex x being Element of M st V = x -neighbour by Def3;
then A2: ( dist p1,p2 = 0 & dist p2,p1 = 0 ) by A1, Th17;
Q is equivalence_class of M by Th26;
then ex y being Element of M st Q = y -neighbour by Def3;
then A3: ( dist q1,q2 = 0 & dist q2,q1 = 0 ) by A1, Th17;
A4: dist p1,q1 <= (dist p1,p2) + (dist p2,q1) by METRIC_1:4;
dist p2,q1 <= (dist p2,q2) + (dist q2,q1) by METRIC_1:4;
then A5: dist p1,q1 <= dist p2,q2 by A2, A3, A4, XXREAL_0:2;
A6: dist p2,q2 <= (dist p2,p1) + (dist p1,q2) by METRIC_1:4;
dist p1,q2 <= (dist p1,q1) + (dist q1,q2) by METRIC_1:4;
then dist p2,q2 <= dist p1,q1 by A2, A3, A6, XXREAL_0:2;
hence dist p1,q1 = dist p2,q2 by A5, XXREAL_0:1; :: thesis: verum