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 set such that
A2: w in P by XBOOLE_0:def 1;
reconsider w = w as Point of M by A2, TOPMETR:16;
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, Th22; :: thesis: verum