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) = max_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) = max_dist_max (P,Q) ) )
assume that
A1: ( P <> {} & P is compact ) and
A2: ( Q <> {} & Q is compact ) ; :: thesis: ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
consider x2 being Point of (TopSpaceMetr M) such that
A3: x2 in Q and
A4: (dist_max P) . x2 = upper_bound ((dist_max P) .: Q) by A1, A2, Th14, Th24;
A5: TopSpaceMetr M = TopStruct(# the carrier of M,(Family_open_set M) #) by PCOMPS_1:def 5;
then reconsider x2 = x2 as Point of M ;
consider x1 being Point of (TopSpaceMetr M) such that
A6: x1 in P and
A7: (dist x2) . x1 = upper_bound ((dist x2) .: P) by A1, Th14, Th16;
reconsider x1 = x1 as Point of M by A5;
take x1 ; :: thesis: ex x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
take x2 ; :: thesis: ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) )
dist (x1,x2) = (dist x2) . x1 by Def4
.= upper_bound ((dist_max P) .: Q) by A4, A7, Def5 ;
hence ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_max (P,Q) ) by A3, A6; :: thesis: verum