let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( S-bound X < S-bound Y implies S-max (X \/ Y) = S-max X )
A1: X \/ Y is compact by COMPTS_1:19;
assume A2: S-bound X < S-bound Y ; :: thesis: S-max (X \/ Y) = S-max X
then A3: S-bound (X \/ Y) = S-bound X by Th25;
A4: ( (S-max (X \/ Y)) `2 = S-bound (X \/ Y) & (S-max X) `2 = S-bound X ) by EUCLID:56;
A5: X c= X \/ Y by XBOOLE_1:7;
S-max X in X by SPRECT_1:14;
then S-max X in S-most (X \/ Y) by A1, A3, A4, A5, SPRECT_2:15;
then A6: (S-max (X \/ Y)) `1 >= (S-max X) `1 by A1, PSCOMP_1:118;
A7: S-max (X \/ Y) in X \/ Y by A1, SPRECT_1:14;

per cases ( S-max (X \/ Y) in X or S-max (X \/ Y) in Y ) by A7, XBOOLE_0:def 3;

suppose S-max (X \/ Y) in X ; :: thesis: S-max (X \/ Y) = S-max X

then S-max (X \/ Y) in S-most X by A2, A4, Th25, SPRECT_2:15;
then (S-max (X \/ Y)) `1 <= (S-max X) `1 by PSCOMP_1:118;
then (S-max (X \/ Y)) `1 = (S-max X) `1 by A6, XXREAL_0:1;
hence S-max (X \/ Y) = S-max X by A2, A4, Th25, TOPREAL3:11; :: thesis: verum

end;

suppose S-max (X \/ Y) in Y ; :: thesis: S-max (X \/ Y) = S-max X

hence S-max (X \/ Y) = S-max X by A2, A3, A4, PSCOMP_1:71; :: thesis: verum

end;

end;