theorem Th7: :: NAGATA_2:7

for T being non empty TopSpace
for pmet being Function of [: the carrier of T, the carrier of T:],REAL st pmet is_a_pseudometric_of the carrier of T holds
for x, y being Point of T
for A being non empty Subset of T holds |.(((lower_bound (pmet,A)) . x) - ((lower_bound (pmet,A)) . y)).| <= pmet . (x,y)