let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( N-bound X < N-bound Y implies N-min (X \/ Y) = N-min Y )
A1: (N-min (X \/ Y)) `2 = N-bound (X \/ Y) by EUCLID:52;
A2: X \/ Y is compact by COMPTS_1:10;
then A3: N-min (X \/ Y) in X \/ Y by SPRECT_1:11;
A4: N-min Y in Y by SPRECT_1:11;
A5: (N-min Y) `2 = N-bound Y by EUCLID:52;
assume A6: N-bound X < N-bound Y ; :: thesis: N-min (X \/ Y) = N-min Y
then A7: N-bound (X \/ Y) = N-bound Y by Th23;
Y c= X \/ Y by XBOOLE_1:7;
then N-min Y in N-most (X \/ Y) by A2, A7, A5, A4, SPRECT_2:10;
then A8: (N-min (X \/ Y)) `1 <= (N-min Y) `1 by A2, PSCOMP_1:39;
per cases ( N-min (X \/ Y) in Y or N-min (X \/ Y) in X ) by A3, XBOOLE_0:def 3;
suppose N-min (X \/ Y) in Y ; :: thesis: N-min (X \/ Y) = N-min Y
then N-min (X \/ Y) in N-most Y by A6, A1, Th23, SPRECT_2:10;
then (N-min (X \/ Y)) `1 >= (N-min Y) `1 by PSCOMP_1:39;
then (N-min (X \/ Y)) `1 = (N-min Y) `1 by A8, XXREAL_0:1;
hence N-min (X \/ Y) = N-min Y by A6, A1, A5, Th23, TOPREAL3:6; :: thesis: verum
end;
suppose N-min (X \/ Y) in X ; :: thesis: N-min (X \/ Y) = N-min Y
hence N-min (X \/ Y) = N-min Y by A6, A7, A1, PSCOMP_1:24; :: thesis: verum
end;
end;