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 that
A1: p1 in V and
A2: q1 in Q and
A3: p2 in V and
A4: 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 A5: dist p1,p2 = 0 by A1, A3, Th17;
Q is equivalence_class of M by Th26;
then ex y being Element of M st Q = y -neighbour by Def3;
then A6: dist q1,q2 = 0 by A2, A4, Th17;
( dist p2,q2 <= (dist p2,p1) + (dist p1,q2) & dist p1,q2 <= (dist p1,q1) + (dist q1,q2) ) by METRIC_1:4;
then A7: dist p2,q2 <= dist p1,q1 by A5, A6, XXREAL_0:2;
( dist p1,q1 <= (dist p1,p2) + (dist p2,q1) & dist p2,q1 <= (dist p2,q2) + (dist q2,q1) ) by METRIC_1:4;
then dist p1,q1 <= dist p2,q2 by A5, A6, XXREAL_0:2;
hence dist p1,q1 = dist p2,q2 by A7, XXREAL_0:1; :: thesis: verum