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