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 |.((upper_bound ((dist p1) .: P)) - (upper_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 |.((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))).| <= dist (p1,p2) )
assume that
A1:
P <> {}
and
A2:
P is compact
; for p1, p2 being Point of M holds |.((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))).| <= dist (p1,p2)
let p1, p2 be Point of M; |.((upper_bound ((dist p1) .: P)) - (upper_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 = upper_bound ((dist p1) .: P)
by A1, A2, Th14, Th16;
A5:
TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #)
by PCOMPS_1:def 5;
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 = upper_bound ((dist p2) .: P)
by A1, A2, Th14, Th16;
reconsider x2 = x2 as Point of M by A5;
A8:
dist (x2,p2) = upper_bound ((dist p2) .: P)
by A7, Def4;
(dist p1) . x1 = dist (x1,p1)
by Def4;
then
( dist (x2,p2) <= (dist (x2,p1)) + (dist (p1,p2)) & dist (x2,p1) <= dist (x1,p1) )
by A2, A4, A6, Th19, METRIC_1:4;
then
(dist (x2,p2)) - (dist (x1,p1)) <= ((dist (x2,p1)) + (dist (p1,p2))) - (dist (x2,p1))
by XREAL_1:13;
then A9:
- (dist (p1,p2)) <= - ((dist (x2,p2)) - (dist (x1,p1)))
by XREAL_1:24;
(dist p2) . x2 = dist (x2,p2)
by Def4;
then
( dist (x1,p1) <= (dist (x1,p2)) + (dist (p2,p1)) & dist (x1,p2) <= dist (x2,p2) )
by A2, A3, A7, Th19, METRIC_1:4;
then A10:
(dist (x1,p1)) - (dist (x2,p2)) <= ((dist (x1,p2)) + (dist (p1,p2))) - (dist (x1,p2))
by XREAL_1:13;
dist (x1,p1) = upper_bound ((dist p1) .: P)
by A4, Def4;
hence
|.((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))).| <= dist (p1,p2)
by A8, A10, A9, ABSVALUE:5; verum