let n be Nat; :: thesis: for A, B being non empty compact Subset of (TOP-REAL n) ex p, q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
let A, B be non empty compact Subset of (TOP-REAL n); :: thesis: ex p, q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
consider A9, B9 being Subset of (TopSpaceMetr (Euclid n)) such that
A1: ( A = A9 & B = B9 ) and
A2: dist_min (A,B) = min_dist_min (A9,B9) by Def1;
TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then ( A9 is compact & B9 is compact ) by A1, COMPTS_1:23;
then consider x1, x2 being Point of (Euclid n) such that
A3: ( x1 in A9 & x2 in B9 ) and
A4: dist (x1,x2) = min_dist_min (A9,B9) by A1, WEIERSTR:30;
reconsider p = x1, q = x2 as Point of (TOP-REAL n) by TOPREAL3:8;
take p ; :: thesis: ex q being Point of (TOP-REAL n) st
( p in A & q in B & dist_min (A,B) = dist (p,q) )
take q ; :: thesis: ( p in A & q in B & dist_min (A,B) = dist (p,q) )
thus ( p in A & q in B ) by A1, A3; :: thesis: dist_min (A,B) = dist (p,q)
thus dist_min (A,B) = dist (p,q) by A2, A4, TOPREAL6:def 1; :: thesis: verum