let A, B be non empty compact Subset of (TOP-REAL n); :: thesis: dist_min A,B = dist_min B,A
consider A', B' being Subset of (TopSpaceMetr (Euclid n)) such that
A1: ( A = A' & B = B' ) and
A2: 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 reconsider A' = A', B' = B' as non empty compact Subset of (TopSpaceMetr (Euclid n)) by A1, COMPTS_1:33;
dist_min A,B = min_dist_min B',A' by A2;
hence dist_min A,B = dist_min B,A by A1, Def1; :: thesis: verum