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 Lm1;
A1: D is compact by Lm1, COMPTS_1:23;
then consider x1, x2 being Point of (Euclid 2) such that
A2: ( x1 in D & x2 in D ) and
A3: dist (x1,x2) = max_dist_max (D,D) by WEIERSTR:33;
reconsider a = x1, b = x2 as Point of (TOP-REAL 2) by EUCLID:67;
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 A2; :: 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 A4: ( x in C & y in C ) ; :: thesis: dist (a,b) >= dist (x,y)
reconsider x9 = x, y9 = y as Point of (Euclid 2) by EUCLID:67;
dist (x9,y9) <= max_dist_max (D,D) by A1, A4, WEIERSTR:34;
then dist (x,y) <= max_dist_max (D,D) by TOPREAL6:def 1;
hence dist (a,b) >= dist (x,y) by A3, TOPREAL6:def 1; :: thesis: verum