let X, Y be non empty compact Subset of (TOP-REAL 2); :: thesis: ( N-bound X < N-bound Y implies N-max (X \/ Y) = N-max Y )
A1: X \/ Y is compact by COMPTS_1:19;
assume A2: N-bound X < N-bound Y ; :: thesis: N-max (X \/ Y) = N-max Y
then A3: N-bound (X \/ Y) = N-bound Y by Th23;
A4: ( (N-max (X \/ Y)) `2 = N-bound (X \/ Y) & (N-max Y) `2 = N-bound Y ) by EUCLID:56;
A5: Y c= X \/ Y by XBOOLE_1:7;
N-max Y in Y by SPRECT_1:13;
then N-max Y in N-most (X \/ Y) by A1, A3, A4, A5, SPRECT_2:14;
then A6: (N-max (X \/ Y)) `1 >= (N-max Y) `1 by A1, PSCOMP_1:98;
A7: N-max (X \/ Y) in X \/ Y by A1, SPRECT_1:13;

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

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

then N-max (X \/ Y) in N-most Y by A2, A4, Th23, SPRECT_2:14;
then (N-max (X \/ Y)) `1 <= (N-max Y) `1 by PSCOMP_1:98;
then (N-max (X \/ Y)) `1 = (N-max Y) `1 by A6, XXREAL_0:1;
hence N-max (X \/ Y) = N-max Y by A2, A4, Th23, TOPREAL3:11; :: thesis: verum

end;

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

hence N-max (X \/ Y) = N-max Y by A2, A3, A4, PSCOMP_1:71; :: thesis: verum

end;

end;