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

proof

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

proof

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

end;

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

end;

E-bound C >= E-bound (Lower_Arc C) by JORDAN6:61, PSCOMP_1:67;
hence E-bound C = E-bound (Lower_Arc C) by A1, XXREAL_0:1; :: thesis: verum