let C be non empty compact Subset of ; :: thesis: ex p1, p2 being Point of st p1,p2 realize-max-dist-in C
reconsider D = C as Subset of by Lm1;
A1: D is compact by Lm1, COMPTS_1:33;
then consider x1, x2 being Point of such that
A2: ( x1 in D & x2 in D ) and
A3: dist x1,x2 = max_dist_max D,D by WEIERSTR:39;
reconsider a = x1, b = x2 as Point of by EUCLID:71;
take a ; :: thesis: ex p2 being Point of 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 st x in C & y in C holds
dist a,b >= dist x,y
let x, y be Point of ; :: 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 x' = x, y' = y as Point of by EUCLID:71;
dist x',y' <= max_dist_max D,D by A1, A4, WEIERSTR:40;
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