let C be Simple_closed_curve; :: thesis: W-bound C = W-bound (Upper_Arc C)
Upper_Arc C c= C by JORDAN6:76;
then A1: W-bound C <= W-bound (Upper_Arc C) by PSCOMP_1:132;
W-bound (Upper_Arc C) <= W-bound C

proof

assume A2: W-bound (Upper_Arc C) > W-bound C ; :: thesis: contradiction
A3: (W-min C) `1 = W-bound C by EUCLID:56;
A4: west_halfline (W-min C) misses Upper_Arc C

proof

assume west_halfline (W-min C) meets Upper_Arc C ; :: thesis: contradiction
then consider p being set such that
A5: p in west_halfline (W-min 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 >= W-bound (Upper_Arc C) by A6, PSCOMP_1:71;
then W-bound C < p `1 by A2, XXREAL_0:2;
hence contradiction by A3, A5, TOPREAL1:def 15; :: thesis: verum

end;

A7: W-min C in west_halfline (W-min C) by TOPREAL1:45;
W-min C in Upper_Arc C by JORDAN7:1;
hence contradiction by A4, A7, XBOOLE_0:3; :: thesis: verum

end;

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