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 Th17;
then ex x being Element of M st V = x -neighbour by Def3;
then A5: dist (p1,p2) = 0 by A1, A3, Th10;
Q is equivalence_class of M by Th17;
then ex y being Element of M st Q = y -neighbour by Def3;
then A6: dist (q1,q2) = 0 by A2, A4, Th10;
( 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