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

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

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

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

end;

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

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

end;

end;