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