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 ((lower_bound ((dist p1) .: P)) - (lower_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 ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2 )
assume A1: ( P <> {} & P is compact ) ; :: thesis: 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; :: thesis: abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2
consider x1 being Point of (TopSpaceMetr M) such that
A2: ( x1 in P & (dist p1) . x1 = lower_bound ((dist p1) .: P) ) by A1, Th21, Th22;
consider x2 being Point of (TopSpaceMetr M) such that
A3: ( x2 in P & (dist p2) . x2 = lower_bound ((dist p2) .: P) ) by A1, Th21, Th22;
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 = lower_bound ((dist p1) .: P) by A2, Def6;
A7: (dist p2) . x2 = dist x2,p2 by Def6;
A8: dist x2,p2 = lower_bound ((dist p2) .: P) by A3, Def6;
A9: ( dist x1,p2 <= (dist x1,p1) + (dist p1,p2) & dist x2,p1 <= (dist x2,p2) + (dist p2,p1) ) by METRIC_1:4;
A10: dist x2,p2 <= dist x1,p2 by A1, A2, A3, A7, Th25;
dist x1,p1 <= dist x2,p1 by A1, A2, A3, A5, Th25;
then dist x1,p1 <= (dist x2,p2) + (dist p1,p2) by A9, XXREAL_0:2;
then A11: (dist x1,p1) - (dist x2,p2) <= dist p1,p2 by XREAL_1:22;
dist x2,p2 <= (dist x1,p1) + (dist p1,p2) by A9, A10, XXREAL_0:2;
then (dist x2,p2) - (dist x1,p1) <= dist p1,p2 by XREAL_1:22;
then - (dist p1,p2) <= - ((dist x2,p2) - (dist x1,p1)) by XREAL_1:26;
hence abs ((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))) <= dist p1,p2 by A6, A8, A11, ABSVALUE:12; :: thesis: verum