let n be Element of 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 A', B' being Subset of (TopSpaceMetr (Euclid n)) such that
A1: A = A' and
A2: B = B' and
A3: dist_min A,B = min_dist_min A',B' by Def1;
TopStruct(# the carrier of (TOP-REAL n),the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) by EUCLID:def 8;
then ( A' is compact & B' is compact ) by A1, A2, COMPTS_1:33;
then consider x1, x2 being Point of (Euclid n) such that
A4: x1 in A' and
A5: x2 in B' and
A6: dist x1,x2 = min_dist_min A',B' by A1, A2, WEIERSTR:36;
reconsider p = x1, q = x2 as Point of (TOP-REAL n) by TOPREAL3:13;
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, A2, A4, A5; :: thesis: dist_min A,B = dist p,q
thus dist_min A,B = dist p,q by A3, A6, TOPREAL6:def 1; :: thesis: verum