let C be Simple_closed_curve; :: thesis: for r being real number 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 number ; :: 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:56;
A2: (E-max C) `1 = E-bound C by EUCLID:56;
assume A3: ( W-bound C <= r & 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, Th64;
then consider x being set such that
A4: x in (Lower_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4;
A5: ( x in Lower_Arc C & x in Vertical_Line r ) by A4, XBOOLE_0:def 4;
reconsider fs = x as Point of (TOP-REAL 2) by A4;
Lower_Arc C c= C by Th76;
then A6: ( S-bound C <= fs `2 & fs `2 <= N-bound C ) by A5, PSCOMP_1:71;
A7: |[r,(S-bound C)]| `1 = r by EUCLID:56
.= fs `1 by A5, Th34 ;
A8: |[r,(N-bound C)]| `1 = r by EUCLID:56
.= fs `1 by A5, Th34 ;
( |[r,(S-bound C)]| `2 = S-bound C & |[r,(N-bound C)]| `2 = N-bound C ) by EUCLID:56;
then x in LSeg |[r,(S-bound C)]|,|[r,(N-bound C)]| by A6, A7, A8, GOBOARD7:8;
hence LSeg |[r,(S-bound C)]|,|[r,(N-bound C)]| meets Lower_Arc C by A5, XBOOLE_0:3; :: thesis: verum