let i, k be Element of NAT ; :: thesis:
let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis:
let p be Point of (TOP-REAL 2); :: thesis:
assume that
A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and
A2: i > 0 and
A3: 1 <= k and
A4: k <= width (Gauge C,i) and
A5: (Gauge C,i) * (Center (Gauge C,i)),k in Upper_Arc (L~ (Cage C,i)) and
A6: p `2 = upper_bound (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (Lower_Arc (L~ (Cage C,i))))) ; :: thesis:
set f = Lower_Seq C,i;
set G = Gauge C,i;
A7: Center (Gauge C,i) <= len (Gauge C,i) by JORDAN1B:14;
4 <= len (Gauge C,i) by JORDAN8:13;
then A8: 1 <= len (Gauge C,i) by XXREAL_0:2;
4 <= len (Gauge C,1) by JORDAN8:13;
then 1 <= len (Gauge C,1) by XXREAL_0:2;
then A9: ((Gauge C,1) * (Center (Gauge C,1)),1) `1 = ((Gauge C,i) * (Center (Gauge C,i)),1) `1 by A2, A8, JORDAN1A:57;
A10: ( 1 <= Center (Gauge C,1) & Center (Gauge C,1) <= len (Gauge C,1) ) by JORDAN1B:12, JORDAN1B:14;
A11: 1 <= Center (Gauge C,i) by JORDAN1B:12;
then A12: ((Gauge C,i) * (Center (Gauge C,i)),k) `1 = ((Gauge C,i) * (Center (Gauge C,i)),1) `1 by A3, A4, A7, GOBOARD5:3;
0 + 1 <= i by A2, NAT_1:13;
then A13: ((Gauge C,1) * (Center (Gauge C,1)),1) `2 <= ((Gauge C,i) * (Center (Gauge C,i)),1) `2 by A11, A7, A10, JORDAN1A:64;
A14: (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) c= (LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis:
assume A15: a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) ; :: thesis:
then reconsider q = a as Point of (TOP-REAL 2) ;
A16: a in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k) by A15, XBOOLE_0:def 4;
A17: a in L~ (Lower_Seq C,i) by A15, XBOOLE_0:def 4;
then q in (L~ (Lower_Seq C,i)) \/ (L~ (Upper_Seq C,i)) by XBOOLE_0:def 3;
then q in L~ (Cage C,i) by JORDAN1E:17;
then S-bound (L~ (Cage C,i)) <= q `2 by PSCOMP_1:71;
then A18: ((Gauge C,i) * (Center (Gauge C,i)),1) `2 <= q `2 by A7, JORDAN1A:93, JORDAN1B:12;
((Gauge C,i) * (Center (Gauge C,i)),1) `2 <= ((Gauge C,i) * (Center (Gauge C,i)),k) `2 by A3, A4, A11, A7, JORDAN1A:40;
then ((Gauge C,1) * (Center (Gauge C,1)),1) `2 <= ((Gauge C,i) * (Center (Gauge C,i)),k) `2 by A13, XXREAL_0:2;
then A19: q `2 <= ((Gauge C,i) * (Center (Gauge C,i)),k) `2 by A16, TOPREAL1:10;
q `1 = ((Gauge C,i) * (Center (Gauge C,i)),1) `1 by A9, A12, A16, GOBOARD7:5;
then q in LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k) by A12, A19, A18, GOBOARD7:8;
hence a in (LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) by A17, XBOOLE_0:def 4; :: thesis:

end;

A20: (Gauge C,i) * (Center (Gauge C,i)),k in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k) by RLTOPSP1:69;
((Gauge C,i) * (Center (Gauge C,i)),1) `2 <= ((Gauge C,i) * (Center (Gauge C,i)),k) `2 by A3, A4, A11, A7, JORDAN1A:40;
then (Gauge C,i) * (Center (Gauge C,i)),1 in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k) by A9, A12, A13, GOBOARD7:8;
then LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k) c= LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k) by A20, TOPREAL1:12;
then (LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) by XBOOLE_1:27;
then (LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) = (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)) by A14, XBOOLE_0:def 10;
then A21: upper_bound (proj2 .: ((LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)))) = upper_bound (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (Lower_Arc (L~ (Cage C,i))))) by A2, JORDAN1G:64;
A22: ( Lower_Seq C,i is_sequence_on Gauge C,i & Upper_Arc (L~ (Cage C,i)) c= L~ (Cage C,i) ) by JORDAN1F:12, JORDAN6:76;
len (Gauge C,i) >= 4 by JORDAN8:13;
then width (Gauge C,i) >= 4 by JORDAN8:def 1;
then 1 <= width (Gauge C,i) by XXREAL_0:2;
then A23: [(Center (Gauge C,i)),1] in Indices (Gauge C,i) by A11, A7, MATRIX_1:37;
[(Center (Gauge C,i)),k] in Indices (Gauge C,i) by A3, A4, A11, A7, MATRIX_1:37;
then consider n being Element of NAT such that
A24: 1 <= n and
A25: n <= k and
A26: ((Gauge C,i) * (Center (Gauge C,i)),n) `2 = upper_bound (proj2 .: ((LSeg ((Gauge C,i) * (Center (Gauge C,i)),1),((Gauge C,i) * (Center (Gauge C,i)),k)) /\ (L~ (Lower_Seq C,i)))) by A3, A4, A5, A11, A7, A23, A22, JORDAN1F:2, JORDAN1G:54;
take n ; :: thesis:
thus 1 <= n by A24; :: thesis:
thus n <= width (Gauge C,i) by A4, A25, XXREAL_0:2; :: thesis:
then p `1 = ((Gauge C,i) * (Center (Gauge C,i)),n) `1 by A1, A2, A24, JORDAN1G:43;
hence p = (Gauge C,i) * (Center (Gauge C,i)),n by A6, A26, A21, TOPREAL3:11; :: thesis: