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 Upper_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 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,(S-bound C)]|,|[r,(N-bound C)]|) 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 (Upper_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4;

A6: x in Upper_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: Upper_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 Upper_Arc C by A6, XBOOLE_0:3; :: thesis: verum

LSeg (|[r,(S-bound C)]|,|[r,(N-bound C)]|) meets Upper_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 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,(S-bound C)]|,|[r,(N-bound C)]|) 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 (Upper_Arc C) /\ (Vertical_Line r) by XBOOLE_0:4;

A6: x in Upper_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: Upper_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 Upper_Arc C by A6, XBOOLE_0:3; :: thesis: verum