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