let M be non empty MetrSpace; 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_min (P,Q) )
let P, Q be Subset of (TopSpaceMetr M); ( 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_min (P,Q) ) )
assume that
A1:
( P <> {} & P is compact )
and
A2:
( Q <> {} & Q is compact )
; ex x1, x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
consider x2 being Point of (TopSpaceMetr M) such that
A3:
x2 in Q
and
A4:
(dist_min P) . x2 = upper_bound ((dist_min P) .: Q)
by A1, A2, Th14, Th27;
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 = lower_bound ((dist x2) .: P)
by A1, Th15, Th16;
reconsider x1 = x1 as Point of M by A5;
take
x1
; ex x2 being Point of M st
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
take
x2
; ( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
dist (x1,x2) =
(dist x2) . x1
by Def4
.=
upper_bound ((dist_min P) .: Q)
by A4, A7, Def6
;
hence
( x1 in P & x2 in Q & dist (x1,x2) = max_dist_min (P,Q) )
by A3, A6; verum