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