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

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

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

then S-min (X \/ Y) in S-most X by A6, A1, Th25, SPRECT_2:11;
then (S-min (X \/ Y)) `1 >= (S-min X) `1 by PSCOMP_1:55;
then (S-min (X \/ Y)) `1 = (S-min X) `1 by A8, XXREAL_0:1;
hence S-min (X \/ Y) = S-min X by A6, A1, A5, Th25, TOPREAL3:6; :: thesis: verum

end;

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

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

end;

end;