let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M st P is compact holds
(dist_min P) . z <= (dist_max P) . z
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for z being Point of M st P is compact holds
(dist_min P) . z <= (dist_max P) . z
let z be Point of M; :: thesis: ( P is compact implies (dist_min P) . z <= (dist_max P) . z )
consider w being Point of M such that
A1: w in P and
A2: (dist_min P) . z <= dist (w,z) by Th19;
assume P is compact ; :: thesis: (dist_min P) . z <= (dist_max P) . z
then (dist_max P) . z >= dist (z,w) by A1, Th20;
hence (dist_min P) . z <= (dist_max P) . z by A2, XXREAL_0:2; :: thesis: verum