let i be Element of 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 & p `2 = lower_bound (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),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 & p `2 = lower_bound (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) holds
ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )
let p be Point of (TOP-REAL 2); :: thesis: ( p `1 = ((W-bound C) + (E-bound C)) / 2 & p `2 = lower_bound (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) implies ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j ) )
assume that
A1: p `1 = ((W-bound C) + (E-bound C)) / 2 and
A2: p `2 = lower_bound (proj2 .: ((LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (Upper_Arc (L~ (Cage C,(i + 1)))))) ; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )

per cases ( ( L~ (Upper_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) & L~ (Lower_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) ) or ( L~ (Upper_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) & L~ (Lower_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) ) ) by Th9;

suppose A3: ( L~ (Upper_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) & L~ (Lower_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) ) ; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )

A4: 1 <= Center (Gauge C,1) by JORDAN1B:12;
set k = width (Gauge C,(i + 1));
set l = Center (Gauge C,(i + 1));
set G = Gauge C,(i + 1);
set f = Upper_Seq C,(i + 1);
A5: 1 <= Center (Gauge C,(i + 1)) by JORDAN1B:12;
A6: width (Gauge C,(i + 1)) = len (Gauge C,(i + 1)) by JORDAN8:def 1;
then width (Gauge C,(i + 1)) >= 4 by JORDAN8:13;
then A7: 1 <= width (Gauge C,(i + 1)) by XXREAL_0:2;
then A8: Center (Gauge C,(i + 1)) <= len (Gauge C,(i + 1)) by A6, JORDAN1B:13;
then A9: ( [(Center (Gauge C,(i + 1))),1] in Indices (Gauge C,(i + 1)) & [(Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))] in Indices (Gauge C,(i + 1)) ) by A7, A5, MATRIX_1:37;
A10: width (Gauge C,1) = len (Gauge C,1) by JORDAN8:def 1;
then width (Gauge C,1) >= 4 by JORDAN8:13;
then A11: 1 <= width (Gauge C,1) by XXREAL_0:2;
then A12: Center (Gauge C,1) <= len (Gauge C,1) by A10, JORDAN1B:13;
A13: (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) c= (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) or a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) )
A14: Upper_Arc (L~ (Cage C,(i + 1))) c= L~ (Cage C,(i + 1)) by JORDAN6:76;
assume A15: a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) ; :: thesis: a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1)))
then reconsider a1 = a as Point of (TOP-REAL 2) ;
A16: a1 in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) by A15, XBOOLE_0:def 4;
a1 in Upper_Arc (L~ (Cage C,(i + 1))) by A3, A15, XBOOLE_0:def 4;
then A17: a1 `2 <= N-bound (L~ (Cage C,(i + 1))) by A14, PSCOMP_1:71;
Cage C,(i + 1) is_sequence_on Gauge C,(i + 1) by JORDAN9:def 1;
then ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2 >= N-bound (L~ (Cage C,(i + 1))) by A6, A7, A5, JORDAN1A:41, JORDAN1B:13;
then A18: a1 `2 <= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2 by A17, XXREAL_0:2;
a1 in Upper_Arc (L~ (Cage C,(i + 1))) by A3, A15, XBOOLE_0:def 4;
then A19: a1 `2 >= S-bound (L~ (Cage C,(i + 1))) by A14, PSCOMP_1:71;
Cage C,(i + 1) is_sequence_on Gauge C,(i + 1) by JORDAN9:def 1;
then ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2 <= S-bound (L~ (Cage C,(i + 1))) by A6, A7, A5, JORDAN1A:43, JORDAN1B:13;
then A20: a1 `2 >= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2 by A19, XXREAL_0:2;
A21: a1 in L~ (Upper_Seq C,(i + 1)) by A15, XBOOLE_0:def 4;
((Gauge C,1) * (Center (Gauge C,1)),1) `1 = ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) `1 by A11, A12, A4, GOBOARD5:3;
then A22: a1 `1 = ((Gauge C,1) * (Center (Gauge C,1)),1) `1 by A16, GOBOARD7:5
.= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `1 by A6, A10, A7, A11, JORDAN1A:57 ;
then a1 `1 = ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `1 by A7, A8, A5, GOBOARD5:3;
then a1 in LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) by A22, A20, A18, GOBOARD7:8;
hence a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) by A21, XBOOLE_0:def 4; :: thesis: verum

end;

1 <= i + 1 by NAT_1:11;
then (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) by A6, A10, JORDAN1A:65, XBOOLE_1:26;
then A23: (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Upper_Seq C,(i + 1))) = (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))) by A13, XBOOLE_0:def 10;
LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) meets L~ (Upper_Seq C,(i + 1)) by A3, A6, A7, A5, JORDAN1B:13, JORDAN1B:32;
then consider n being Element of NAT such that
A24: ( 1 <= n & n <= width (Gauge C,(i + 1)) ) and
A25: ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `2 = lower_bound (proj2 .: ((LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Upper_Seq C,(i + 1))))) by A7, A9, Th1, Th10;
take n ; :: thesis: ( 1 <= n & n <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n )
thus ( 1 <= n & n <= width (Gauge C,(i + 1)) ) by A24; :: thesis: p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n
len (Gauge C,1) >= 4 by JORDAN8:13;
then A26: 1 <= len (Gauge C,1) by XXREAL_0:2;
then p `1 = ((Gauge C,1) * (Center (Gauge C,1)),1) `1 by A1, JORDAN1A:59
.= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `1 by A6, A24, A26, JORDAN1A:57 ;
hence p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n by A2, A3, A25, A23, TOPREAL3:11; :: thesis: verum

end;

suppose A27: ( L~ (Upper_Seq C,(i + 1)) = Lower_Arc (L~ (Cage C,(i + 1))) & L~ (Lower_Seq C,(i + 1)) = Upper_Arc (L~ (Cage C,(i + 1))) ) ; :: thesis: ex j being Element of NAT st
( 1 <= j & j <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),j )

A28: 1 <= Center (Gauge C,1) by JORDAN1B:12;
set k = width (Gauge C,(i + 1));
set l = Center (Gauge C,(i + 1));
set G = Gauge C,(i + 1);
set f = Lower_Seq C,(i + 1);
A29: 1 <= Center (Gauge C,(i + 1)) by JORDAN1B:12;
A30: width (Gauge C,(i + 1)) = len (Gauge C,(i + 1)) by JORDAN8:def 1;
then width (Gauge C,(i + 1)) >= 4 by JORDAN8:13;
then A31: 1 <= width (Gauge C,(i + 1)) by XXREAL_0:2;
then A32: Center (Gauge C,(i + 1)) <= len (Gauge C,(i + 1)) by A30, JORDAN1B:13;
then A33: ( [(Center (Gauge C,(i + 1))),1] in Indices (Gauge C,(i + 1)) & [(Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))] in Indices (Gauge C,(i + 1)) ) by A31, A29, MATRIX_1:37;
A34: width (Gauge C,1) = len (Gauge C,1) by JORDAN8:def 1;
then width (Gauge C,1) >= 4 by JORDAN8:13;
then A35: 1 <= width (Gauge C,1) by XXREAL_0:2;
then A36: Center (Gauge C,1) <= len (Gauge C,1) by A34, JORDAN1B:13;
A37: (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) c= (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) or a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) )
A38: Upper_Arc (L~ (Cage C,(i + 1))) c= L~ (Cage C,(i + 1)) by JORDAN6:76;
assume A39: a in (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) ; :: thesis: a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1)))
then reconsider a1 = a as Point of (TOP-REAL 2) ;
A40: a1 in LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) by A39, XBOOLE_0:def 4;
a1 in Upper_Arc (L~ (Cage C,(i + 1))) by A27, A39, XBOOLE_0:def 4;
then A41: a1 `2 <= N-bound (L~ (Cage C,(i + 1))) by A38, PSCOMP_1:71;
Cage C,(i + 1) is_sequence_on Gauge C,(i + 1) by JORDAN9:def 1;
then ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2 >= N-bound (L~ (Cage C,(i + 1))) by A30, A31, A29, JORDAN1A:41, JORDAN1B:13;
then A42: a1 `2 <= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `2 by A41, XXREAL_0:2;
a1 in Upper_Arc (L~ (Cage C,(i + 1))) by A27, A39, XBOOLE_0:def 4;
then A43: a1 `2 >= S-bound (L~ (Cage C,(i + 1))) by A38, PSCOMP_1:71;
Cage C,(i + 1) is_sequence_on Gauge C,(i + 1) by JORDAN9:def 1;
then ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2 <= S-bound (L~ (Cage C,(i + 1))) by A30, A31, A29, JORDAN1A:43, JORDAN1B:13;
then A44: a1 `2 >= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `2 by A43, XXREAL_0:2;
A45: a1 in L~ (Lower_Seq C,(i + 1)) by A39, XBOOLE_0:def 4;
((Gauge C,1) * (Center (Gauge C,1)),1) `1 = ((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1))) `1 by A35, A36, A28, GOBOARD5:3;
then A46: a1 `1 = ((Gauge C,1) * (Center (Gauge C,1)),1) `1 by A40, GOBOARD7:5
.= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1) `1 by A30, A34, A31, A35, JORDAN1A:57 ;
then a1 `1 = ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) `1 by A31, A32, A29, GOBOARD5:3;
then a1 in LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) by A46, A44, A42, GOBOARD7:8;
hence a in (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) by A45, XBOOLE_0:def 4; :: thesis: verum

end;

1 <= i + 1 by NAT_1:11;
then (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) c= (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) by A30, A34, JORDAN1A:65, XBOOLE_1:26;
then A47: (LSeg ((Gauge C,1) * (Center (Gauge C,1)),1),((Gauge C,1) * (Center (Gauge C,1)),(width (Gauge C,1)))) /\ (L~ (Lower_Seq C,(i + 1))) = (LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))) by A37, XBOOLE_0:def 10;
LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1)))) meets L~ (Lower_Seq C,(i + 1)) by A27, A30, A31, A29, JORDAN1B:13, JORDAN1B:32;
then consider n being Element of NAT such that
A48: ( 1 <= n & n <= width (Gauge C,(i + 1)) ) and
A49: ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `2 = lower_bound (proj2 .: ((LSeg ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),1),((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),(width (Gauge C,(i + 1))))) /\ (L~ (Lower_Seq C,(i + 1))))) by A31, A33, Th1, Th12;
take n ; :: thesis: ( 1 <= n & n <= width (Gauge C,(i + 1)) & p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n )
thus ( 1 <= n & n <= width (Gauge C,(i + 1)) ) by A48; :: thesis: p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n
len (Gauge C,1) >= 4 by JORDAN8:13;
then A50: 1 <= len (Gauge C,1) by XXREAL_0:2;
then p `1 = ((Gauge C,1) * (Center (Gauge C,1)),1) `1 by A1, JORDAN1A:59
.= ((Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n) `1 by A30, A48, A50, JORDAN1A:57 ;
hence p = (Gauge C,(i + 1)) * (Center (Gauge C,(i + 1))),n by A2, A27, A49, A47, TOPREAL3:11; :: thesis: verum

end;

end;