theorem Th22: :: WEIERSTR:22

for M being non empty MetrSpace
for P being Subset of (TopSpaceMetr M) st P <> {} & P is compact holds
for p1, p2 being Point of M holds |.((lower_bound ((dist p1) .: P)) - (lower_bound ((dist p2) .: P))).| <= dist (p1,p2)