let C be Simple_closed_curve; :: thesis: E-bound C = E-bound (Lower_Arc C)
Lower_Arc C c= C by JORDAN6:76;
then A1: E-bound C >= E-bound (Lower_Arc C) by PSCOMP_1:130;
E-bound (Lower_Arc C) >= E-bound C

proof

assume A2: E-bound (Lower_Arc C) < E-bound C ; :: thesis: contradiction
A3: (E-max C) `1 = E-bound C by EUCLID:56;
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 set 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:71;
then E-bound C > p `1 by A2, XXREAL_0:2;
hence contradiction by A3, A5, TOPREAL1:def 13; :: thesis: verum

end;

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

end;

hence E-bound C = E-bound (Lower_Arc C) by A1, XXREAL_0:1; :: thesis: verum