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 and
A2: y2 in P and
A3: dist y1,y2 = min_dist_min Q,P by WEIERSTR:36;
consider x1, x2 being Point of M such that
A4: x1 in P and
A5: x2 in Q and
A6: dist x1,x2 = min_dist_min P,Q by WEIERSTR:36;
A7: dist x1,x2 <= dist y1,y2 by A1, A2, A6, WEIERSTR:40;
dist y1,y2 <= dist x1,x2 by A3, A4, A5, WEIERSTR:40;
hence min_dist_min P,Q = min_dist_min Q,P by A3, A6, A7, XXREAL_0:1; :: thesis: verum