let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( W-bound X < W-bound Y implies W-max (X \/ Y) = W-max X )
A1: (W-max (X \/ Y)) `1 = W-bound (X \/ Y) by EUCLID:52;
A2: X \/ Y is compact by COMPTS_1:10;
then A3: W-max (X \/ Y) in X \/ Y by SPRECT_1:13;
A4: W-max X in X by SPRECT_1:13;
A5: (W-max X) `1 = W-bound X by EUCLID:52;
assume A6: W-bound X < W-bound Y ; :: thesis: W-max (X \/ Y) = W-max X
then A7: W-bound (X \/ Y) = W-bound X by Th26;
X c= X \/ Y by XBOOLE_1:7;
then W-max X in W-most (X \/ Y) by A2, A7, A5, A4, SPRECT_2:12;
then A8: (W-max (X \/ Y)) `2 >= (W-max X) `2 by A2, PSCOMP_1:31;

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

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

then W-max (X \/ Y) in W-most X by A6, A1, Th26, SPRECT_2:12;
then (W-max (X \/ Y)) `2 <= (W-max X) `2 by PSCOMP_1:31;
then (W-max (X \/ Y)) `2 = (W-max X) `2 by A8, XXREAL_0:1;
hence W-max (X \/ Y) = W-max X by A6, A1, A5, Th26, TOPREAL3:6; :: thesis: verum

end;

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

hence W-max (X \/ Y) = W-max X by A6, A7, A1, PSCOMP_1:24; :: thesis: verum

end;

end;