theorem Th20: :: WEIERSTR:20

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 |.((upper_bound ((dist p1) .: P)) - (upper_bound ((dist p2) .: P))).| <= dist (p1,p2)