let M be PseudoMetricSpace; 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 ; 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; ( 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
; 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; verum