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:36;
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:36;
( dist x1,x2 <= dist y1,y2 & dist y1,y2 <= dist x1,x2 ) by A1, A2, A3, A4, WEIERSTR:40;
hence min_dist_min P,Q = min_dist_min Q,P by A2, A4, XXREAL_0:1; :: thesis: verum