let M be non empty MetrSpace; for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2
let P be Subset of (TopSpaceMetr M); ( P <> {} & P is compact implies for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2 )
assume that
A1:
P <> {}
and
A2:
P is compact
; for p1, p2 being Point of M holds abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2
let p1, p2 be Point of M; abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2
consider x1 being Point of (TopSpaceMetr M) such that
A3:
x1 in P
and
A4:
(dist p1) . x1 = lower_bound ((dist p1) .: P)
by A1, A2, Th21, Th22;
A5:
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #)
by PCOMPS_1:def 6;
then reconsider x1 = x1 as Point of M ;
consider x2 being Point of (TopSpaceMetr M) such that
A6:
x2 in P
and
A7:
(dist p2) . x2 = lower_bound ((dist p2) .: P)
by A1, A2, Th21, Th22;
reconsider x2 = x2 as Point of M by A5;
A8:
dist x2,p2 = lower_bound ((dist p2) .: P)
by A7, Def6;
(dist p2) . x2 = dist x2,p2
by Def6;
then
( dist x1,p2 <= (dist x1,p1) + (dist p1,p2) & dist x2,p2 <= dist x1,p2 )
by A2, A3, A7, Th25, METRIC_1:4;
then
dist x2,p2 <= (dist x1,p1) + (dist p1,p2)
by XXREAL_0:2;
then
(dist x2,p2) - (dist x1,p1) <= dist p1,p2
by XREAL_1:22;
then A9:
- (dist p1,p2) <= - ((dist x2,p2) - (dist x1,p1))
by XREAL_1:26;
(dist p1) . x1 = dist x1,p1
by Def6;
then
( dist x2,p1 <= (dist x2,p2) + (dist p2,p1) & dist x1,p1 <= dist x2,p1 )
by A2, A4, A6, Th25, METRIC_1:4;
then
dist x1,p1 <= (dist x2,p2) + (dist p1,p2)
by XXREAL_0:2;
then A10:
(dist x1,p1) - (dist x2,p2) <= dist p1,p2
by XREAL_1:22;
dist x1,p1 = lower_bound ((dist p1) .: P)
by A4, Def6;
hence
abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2
by A8, A10, A9, ABSVALUE:12; verum