let P, Q be non empty compact Subset of (TopSpaceMetr M); :: thesis: min_dist_min (P,Q) = min_dist_min (Q,P)
consider y1, y2 being Point of M such that
A1: ( y1 in Q & y2 in P ) and
A2: dist (y1,y2) = min_dist_min (Q,P) by WEIERSTR:30;
consider x1, x2 being Point of M such that
A3: ( x1 in P & x2 in Q ) and
A4: dist (x1,x2) = min_dist_min (P,Q) by WEIERSTR:30;
( dist (x1,x2) <= dist (y1,y2) & dist (y1,y2) <= dist (x1,x2) ) by A1, A2, A3, A4, WEIERSTR:34;
hence min_dist_min (P,Q) = min_dist_min (Q,P) by A2, A4, XXREAL_0:1; :: thesis: verum