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;
reconsider A' = A', B' = B' as non empty compact Subset of (TopSpaceMetr (Euclid n)) by A1;
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