let M be non empty MetrSpace; :: thesis: for P, Q being Subset of (TopSpaceMetr M) st P <> {} & P is compact & Q <> {} & Q is compact holds
ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist x1,x2 = min_dist_max P,Q )
let P, Q be Subset of (TopSpaceMetr M); :: thesis: ( P <> {} & P is compact & Q <> {} & Q is compact implies ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist x1,x2 = min_dist_max P,Q ) )
assume A1: ( P <> {} & P is compact & Q <> {} & Q is compact ) ; :: thesis: ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist x1,x2 = min_dist_max P,Q )
then consider x2 being Point of (TopSpaceMetr M) such that
A2: ( x2 in Q & (dist_max P) . x2 = lower_bound ((dist_max P) .: Q) ) by Th21, Th30;
A3: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 6;
then reconsider x2 = x2 as Point of M ;
consider x1 being Point of (TopSpaceMetr M) such that
A4: ( x1 in P & (dist x2) . x1 = upper_bound ((dist x2) .: P) ) by A1, Th22, Th20;
reconsider x1 = x1 as Point of M by A3;
take x1 ; :: thesis: ex x2 being Point of M st
( x1 in P & x2 in Q & dist x1,x2 = min_dist_max P,Q )
take x2 ; :: thesis: ( x1 in P & x2 in Q & dist x1,x2 = min_dist_max P,Q )
dist x1,x2 = (dist x2) . x1 by Def6
.= lower_bound ((dist_max P) .: Q) by A2, A4, Def7 ;
hence ( x1 in P & x2 in Q & dist x1,x2 = min_dist_max P,Q ) by A2, A4; :: thesis: verum