let C be Simple_closed_curve; :: thesis: for r being Real st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,()]|,|[r,()]|) meets Upper_Arc C

let r be Real; :: thesis: ( W-bound C <= r & r <= E-bound C implies LSeg (|[r,()]|,|[r,()]|) meets Upper_Arc C )
A1: (W-min C) `1 = W-bound C by EUCLID:52;
A2: (E-max C) `1 = E-bound C by EUCLID:52;
assume that
A3: W-bound C <= r and
A4: r <= E-bound C ; :: thesis: LSeg (|[r,()]|,|[r,()]|) meets Upper_Arc C
Upper_Arc C is_an_arc_of W-min C, E-max C by Def8;
then Upper_Arc C meets Vertical_Line r by A1, A2, A3, A4, Th49;
then consider x being object such that
A5: x in () /\ () by XBOOLE_0:4;
A6: x in Upper_Arc C by ;
A7: x in Vertical_Line r by ;
reconsider fs = x as Point of () by A5;
A8: Upper_Arc C c= C by Th61;
then A9: S-bound C <= fs `2 by ;
A10: fs `2 <= N-bound C by ;
A11: |[r,()]| `1 = r by EUCLID:52
.= fs `1 by ;
A12: |[r,()]| `1 = r by EUCLID:52
.= fs `1 by ;
A13: |[r,()]| `2 = S-bound C by EUCLID:52;
|[r,()]| `2 = N-bound C by EUCLID:52;
then x in LSeg (|[r,()]|,|[r,()]|) by ;
hence LSeg (|[r,()]|,|[r,()]|) meets Upper_Arc C by ; :: thesis: verum