let P be compact Subset of (TOP-REAL 2); ( |[(- 1),0]|,|[1,0]| realize-max-dist-in P implies ( E-min P = |[1,0]| & E-max P = |[1,0]| ) )
set M = E-most P;
assume A1:
|[(- 1),0]|,|[1,0]| realize-max-dist-in P
; ( E-min P = |[1,0]| & E-max P = |[1,0]| )
then A2:
E-most P = {|[1,0]|}
by Th78;
set f = proj2 | (E-most P);
A3:
dom (proj2 | (E-most P)) = the carrier of ((TOP-REAL 2) | (E-most P))
by FUNCT_2:def 1;
A4:
the carrier of ((TOP-REAL 2) | (E-most P)) = E-most P
by PRE_TOPC:8;
A5:
|[1,0]| in {|[1,0]|}
by TARSKI:def 1;
A6: (proj2 | (E-most P)) .: the carrier of ((TOP-REAL 2) | (E-most P)) =
Im ((proj2 | (E-most P)),|[1,0]|)
by A1, A4, Th78
.=
{((proj2 | (E-most P)) . |[1,0]|)}
by A2, A3, A4, A5, FUNCT_1:59
.=
{(proj2 . |[1,0]|)}
by A2, A5, FUNCT_1:49
.=
{(|[1,0]| `2)}
by PSCOMP_1:def 6
;
then A7:
lower_bound (proj2 | (E-most P)) = |[1,0]| `2
by SEQ_4:9;
A8:
upper_bound (proj2 | (E-most P)) = |[1,0]| `2
by A6, SEQ_4:9;
|[1,0]| = |[(|[1,0]| `1),(|[1,0]| `2)]|
by EUCLID:53;
hence
( E-min P = |[1,0]| & E-max P = |[1,0]| )
by A1, A7, A8, Lm17, Th76; verum