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:33;
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:33;
( dist (x1,x2) <= dist (y1,y2) & dist (y1,y2) <= dist (x1,x2) ) by A5, A6, A7, A8, WEIERSTR:34;
hence max_dist_max (P,Q) = max_dist_max (Q,P) by A6, A8, XXREAL_0:1; :: thesis: verum