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

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

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

then E-max (X \/ Y) in E-most Y by A6, A1, Th24, SPRECT_2:13;
then (E-max (X \/ Y)) `2 <= (E-max Y) `2 by PSCOMP_1:47;
then (E-max (X \/ Y)) `2 = (E-max Y) `2 by A8, XXREAL_0:1;
hence E-max (X \/ Y) = E-max Y by A6, A1, A5, Th24, TOPREAL3:6; :: thesis: verum

end;

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

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

end;

end;