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
ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) )
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for z being Point of M st P is compact holds
ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) )
let z be Point of M; :: thesis: ( P is compact implies ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) ) )
assume A1: P is compact ; :: thesis: ex w being Point of M st
( w in P & (dist_max P) . z >= dist (w,z) )
consider w being object such that
A2: w in P by XBOOLE_0:def 1;
reconsider w = w as Point of M by A2, TOPMETR:12;
take w ; :: thesis: ( w in P & (dist_max P) . z >= dist (w,z) )
thus w in P by A2; :: thesis: (dist_max P) . z >= dist (w,z)
thus (dist_max P) . z >= dist (w,z) by A1, A2, Th20; :: thesis: verum