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