let C be Simple_closed_curve; :: thesis: W-bound C = W-bound (Upper_Arc C)
A1: W-bound (Upper_Arc C) <= W-bound C
proof
A2: (W-min C) `1 = W-bound C by EUCLID:52;
assume A3: W-bound (Upper_Arc C) > W-bound C ; :: thesis: contradiction
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 object 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:24;
then W-bound C < p `1 by A3, XXREAL_0:2;
hence contradiction by A2, A5, TOPREAL1:def 13; :: thesis: verum
end;
( W-min C in west_halfline (W-min C) & W-min C in Upper_Arc C ) by JORDAN7:1, TOPREAL1:38;
hence contradiction by A4, XBOOLE_0:3; :: thesis: verum
end;
W-bound C <= W-bound (Upper_Arc C) by JORDAN6:61, PSCOMP_1:69;
hence W-bound C = W-bound (Upper_Arc C) by A1, XXREAL_0:1; :: thesis: verum