let X, Y be non empty compact Subset of (TOP-REAL 2); ( X c= Y & ( E-min Y in X or E-max Y in X ) implies E-bound X = E-bound Y )
assume that
A1:
X c= Y
and
A2:
( E-min Y in X or E-max Y in X )
; E-bound X = E-bound Y
A3:
(E-max X) `1 = E-bound X
by EUCLID:52;
A4:
(E-max Y) `1 = E-bound Y
by EUCLID:52;
A5:
(E-min Y) `1 = E-bound Y
by EUCLID:52;
(E-min X) `1 = E-bound X
by EUCLID:52;
hence
E-bound X = E-bound Y
by A1, A2, A3, A5, A4, Th17, Th18; verum