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