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: X \/ Y is compact by COMPTS_1:19;
assume A2: W-bound X < W-bound Y ; :: thesis: W-min (X \/ Y) = W-min X
then A3: W-bound (X \/ Y) = W-bound X by Th26;
A4: ( (W-min (X \/ Y)) `1 = W-bound (X \/ Y) & (W-min X) `1 = W-bound X ) by EUCLID:56;
A5: X c= X \/ Y by XBOOLE_1:7;
W-min X in X by SPRECT_1:15;
then W-min X in W-most (X \/ Y) by A1, A3, A4, A5, SPRECT_2:16;
then A6: (W-min (X \/ Y)) `2 <= (W-min X) `2 by A1, PSCOMP_1:88;
A7: W-min (X \/ Y) in X \/ Y by A1, SPRECT_1:15;

per cases ( W-min (X \/ Y) in X or W-min (X \/ Y) in Y ) by A7, 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 A2, A4, Th26, SPRECT_2:16;
then (W-min (X \/ Y)) `2 >= (W-min X) `2 by PSCOMP_1:88;
then (W-min (X \/ Y)) `2 = (W-min X) `2 by A6, XXREAL_0:1;
hence W-min (X \/ Y) = W-min X by A2, A4, Th26, TOPREAL3:11; :: 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 A2, A3, A4, PSCOMP_1:71; :: thesis: verum

end;

end;