let M be non empty MetrSpace; :: thesis: for P being non empty Subset of (TopSpaceMetr M)
for z being Point of M ex w being Point of M st
( w in P & (dist_min P) . z <= dist (w,z) )
let P be non empty Subset of (TopSpaceMetr M); :: thesis: for z being Point of M ex w being Point of M st
( w in P & (dist_min P) . z <= dist (w,z) )
let z be Point of M; :: thesis: ex w being Point of M st
( w in P & (dist_min P) . z <= dist (w,z) )
consider w being object such that
A1: w in P by XBOOLE_0:def 1;
reconsider w = w as Point of M by A1, TOPMETR:12;
take w ; :: thesis: ( w in P & (dist_min P) . z <= dist (w,z) )
thus w in P by A1; :: thesis: (dist_min P) . z <= dist (w,z)
thus (dist_min P) . z <= dist (w,z) by A1, Th13; :: thesis: verum