let C be Simple_closed_curve; :: thesis: E-bound C = E-bound (Upper_Arc C)
A1: E-bound (Upper_Arc C) >= E-bound C

proof

A2: (E-max C) `1 = E-bound C by EUCLID:56;
assume A3: E-bound (Upper_Arc C) < E-bound C ; :: thesis: contradiction
A4: east_halfline (E-max C) misses Upper_Arc C

proof

assume east_halfline (E-max C) meets Upper_Arc C ; :: thesis: contradiction
then consider p being set such that
A5: p in east_halfline (E-max C) and
A6: p in Upper_Arc C by XBOOLE_0:3;
reconsider p = p as Point of (TOP-REAL 2) by A5;
p `1 <= E-bound (Upper_Arc C) by A6, PSCOMP_1:71;
then E-bound C > p `1 by A3, XXREAL_0:2;
hence contradiction by A2, A5, TOPREAL1:def 13; :: thesis: verum

end;

( E-max C in east_halfline (E-max C) & E-max C in Upper_Arc C ) by JORDAN7:1, TOPREAL1:45;
hence contradiction by A4, XBOOLE_0:3; :: thesis: verum

end;

E-bound C >= E-bound (Upper_Arc C) by JORDAN6:76, PSCOMP_1:130;
hence E-bound C = E-bound (Upper_Arc C) by A1, XXREAL_0:1; :: thesis: verum