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:23;
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