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
A8: y1 in Q and
A9: y2 in P and
A10: dist y1,y2 = max_dist_max Q,P by WEIERSTR:39;
consider x1, x2 being Point of M such that
A11: x1 in P and
A12: x2 in Q and
A13: dist x1,x2 = max_dist_max P,Q by WEIERSTR:39;
A14: dist x1,x2 <= dist y1,y2 by A10, A11, A12, WEIERSTR:40;
dist y1,y2 <= dist x1,x2 by A8, A9, A13, WEIERSTR:40;
hence max_dist_max P,Q = max_dist_max Q,P by A10, A13, A14, XXREAL_0:1; :: thesis: verum