let P, Q be non empty compact Subset of (TopSpaceMetr M); :: thesis: max_dist_max P,Q = max_dist_max Q,P
consider y1, y2 being Point of M such that
A5: ( y1 in Q & y2 in P ) and
A6: dist y1,y2 = max_dist_max Q,P by WEIERSTR:39;
consider x1, x2 being Point of M such that
A7: ( x1 in P & x2 in Q ) and
A8: dist x1,x2 = max_dist_max P,Q by WEIERSTR:39;
( dist x1,x2 <= dist y1,y2 & dist y1,y2 <= dist x1,x2 ) by A5, A6, A7, A8, WEIERSTR:40;
hence max_dist_max P,Q = max_dist_max Q,P by A6, A8, XXREAL_0:1; :: thesis: verum