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