let i, k be Nat; :: thesis: for C being non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2)
for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & 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)))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
let C be non empty being_simple_closed_curve compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for p being Point of (TOP-REAL 2) st p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & 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)))))) holds
ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & i > 0 & 1 <= k & k <= width (Gauge (C,i)) & (Gauge (C,i)) * ((Center (Gauge (C,i))),k) in Upper_Arc (L~ (Cage (C,i))) & 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)))))) implies ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) ) )
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: ex j being Nat st
( 1 <= j & j <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),j) )
set f = Lower_Seq (C,i);
set G = Gauge (C,i);
A7: Center (Gauge (C,i)) <= len (Gauge (C,i)) by JORDAN1B:13;
4 <= len (Gauge (C,i)) by JORDAN8:10;
then A8: 1 <= len (Gauge (C,i)) by XXREAL_0:2;
4 <= len (Gauge (C,1)) by JORDAN8:10;
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:36;
A10: ( 1 <= Center (Gauge (C,1)) & Center (Gauge (C,1)) <= len (Gauge (C,1)) ) by JORDAN1B:11, JORDAN1B:13;
A11: 1 <= Center (Gauge (C,i)) by JORDAN1B:11;
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:2;
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:43;
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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg (((Gauge (C,1)) * ((Center (Gauge (C,1))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) or a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i))) )
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: a in (LSeg (((Gauge (C,i)) * ((Center (Gauge (C,i))),1)),((Gauge (C,i)) * ((Center (Gauge (C,i))),k)))) /\ (L~ (Lower_Seq (C,i)))
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:13;
then S-bound (L~ (Cage (C,i))) <= q `2 by PSCOMP_1:24;
then A18: ((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= q `2 by A7, JORDAN1A:72, JORDAN1B:11;
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;
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:4;
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:7;
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: verum

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:68;
((Gauge (C,i)) * ((Center (Gauge (C,i))),1)) `2 <= ((Gauge (C,i)) * ((Center (Gauge (C,i))),k)) `2 by A3, A4, A11, A7, JORDAN1A:19;
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:7;
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:6;
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:56;
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:61;
len (Gauge (C,i)) >= 4 by JORDAN8:10;
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_0:30;
[(Center (Gauge (C,i))),k] in Indices (Gauge (C,i)) by A3, A4, A11, A7, MATRIX_0:30;
then consider n being 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:46;
take n ; :: thesis: ( 1 <= n & n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )
thus 1 <= n by A24; :: thesis: ( n <= width (Gauge (C,i)) & p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) )
thus n <= width (Gauge (C,i)) by A4, A25, XXREAL_0:2; :: thesis: p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n)
then p `1 = ((Gauge (C,i)) * ((Center (Gauge (C,i))),n)) `1 by A1, A2, A24, JORDAN1G:35;
hence p = (Gauge (C,i)) * ((Center (Gauge (C,i))),n) by A6, A26, A21, TOPREAL3:6; :: thesis: verum