let P, Q be non empty compact Subset of (TopSpaceMetr M); 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; verum