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 that
A1: X c= Y and
A2: ( S-min Y in X or S-max Y in X ) ; :: thesis: S-bound X = S-bound Y
A3: (S-max X) `2 = S-bound X by EUCLID:52;
A4: (S-max Y) `2 = S-bound Y by EUCLID:52;
A5: (S-min Y) `2 = S-bound Y by EUCLID:52;
(S-min X) `2 = S-bound X by EUCLID:52;
hence S-bound X = S-bound Y by A1, A2, A3, A5, A4, Th19, Th20; :: thesis: verum