let C be non empty compact Subset of (TOP-REAL 2); :: thesis: ex p1, p2 being Point of (TOP-REAL 2) st p1,p2 realize-max-dist-in C
reconsider D = C as Subset of (TopSpaceMetr (Euclid 2)) by XX;
X: D is compact by COMPTS_1:33, XX;
then consider x1, x2 being Point of (Euclid 2) such that
A1: ( x1 in D & x2 in D & dist x1,x2 = max_dist_max D,D ) by WEIERSTR:39;
reconsider a = x1, b = x2 as Point of (TOP-REAL 2) by EUCLID:71;
take a ; :: thesis: ex p2 being Point of (TOP-REAL 2) st a,p2 realize-max-dist-in C
take b ; :: thesis: a,b realize-max-dist-in C
thus ( a in C & b in C ) by A1; :: according to JORDAN24:def 1 :: thesis: for x, y being Point of (TOP-REAL 2) st x in C & y in C holds
dist a,b >= dist x,y
let x, y be Point of (TOP-REAL 2); :: thesis: ( x in C & y in C implies dist a,b >= dist x,y )
assume A2: ( x in C & y in C ) ; :: thesis: dist a,b >= dist x,y
reconsider x' = x, y' = y as Point of (Euclid 2) by EUCLID:71;
dist x',y' <= max_dist_max D,D by A2, WEIERSTR:40, X;
then dist x,y <= max_dist_max D,D by TOPREAL6:def 1;
hence dist a,b >= dist x,y by A1, TOPREAL6:def 1; :: thesis: verum