let C be Simple_closed_curve; :: thesis: for r being Real st W-bound C <= r & r <= E-bound C holds
LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C
let r be Real; :: thesis: ( W-bound C <= r & r <= E-bound C implies LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_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,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C
Lower_Arc C is_an_arc_of E-max C, W-min C by Def9;
then Lower_Arc C is_an_arc_of W-min C, E-max C by JORDAN5B:14;
then Lower_Arc C meets Vertical_Line r by A1, A2, A3, A4, Th49;
then consider x being object such that
A5: x in (Lower_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4;
A6: x in Lower_Arc C by A5, XBOOLE_0:def 4;
A7: x in Vertical_Line r by A5, XBOOLE_0:def 4;
reconsider fs = x as Point of (TOP-REAL 2) by A5;
A8: Lower_Arc C c= C by Th61;
then A9: S-bound C <= fs `2 by A6, PSCOMP_1:24;
A10: fs `2 <= N-bound C by A6, A8, PSCOMP_1:24;
A11: |[r,(S-bound C)]| `1 = r by EUCLID:52
.= fs `1 by A7, Th31 ;
A12: |[r,(N-bound C)]| `1 = r by EUCLID:52
.= fs `1 by A7, Th31 ;
A13: |[r,(S-bound C)]| `2 = S-bound C by EUCLID:52;
|[r,(N-bound C)]| `2 = N-bound C by EUCLID:52;
then x in LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) by A9, A10, A11, A12, A13, GOBOARD7:7;
hence LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Lower_Arc C by A6, XBOOLE_0:3; :: thesis: verum