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:29;
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:117
.=
{(proj2 . |[1,0 ]|)}
by A2, A5, FUNCT_1:72
.=
{(|[1,0 ]| `2 )}
by PSCOMP_1:def 29
;
then A7:
lower_bound (proj2 | (E-most P)) = |[1,0 ]| `2
by SEQ_4:22;
A8:
upper_bound (proj2 | (E-most P)) = |[1,0 ]| `2
by A6, SEQ_4:22;
|[1,0 ]| = |[(|[1,0 ]| `1 ),(|[1,0 ]| `2 )]|
by EUCLID:57;
hence
( E-min P = |[1,0 ]| & E-max P = |[1,0 ]| )
by A1, A7, A8, Lm17, Th76; verum