let i 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 & 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 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 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 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 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 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:11;
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:11;
A6: width (Gauge (C,(i + 1))) = len (Gauge (C,(i + 1))) by JORDAN8:def 1;
then width (Gauge (C,(i + 1))) >= 4 by JORDAN8:10;
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:12;
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_0:30;
A10: width (Gauge (C,1)) = len (Gauge (C,1)) by JORDAN8:def 1;
then width (Gauge (C,1)) >= 4 by JORDAN8:10;
then A11: 1 <= width (Gauge (C,1)) by XXREAL_0:2;
then A12: Center (Gauge (C,1)) <= len (Gauge (C,1)) by A10, JORDAN1B:12;
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 object ; :: 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:61;
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:24;
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:20, JORDAN1B:12;
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:24;
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:22, JORDAN1B:12;
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:2;
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:36 ;
then a1 `1 = ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 by A7, A8, A5, GOBOARD5:2;
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:7;
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:44, 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:12, JORDAN1B:29;
then consider n being 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:10;
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:38
.= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 by A6, A24, A26, JORDAN1A:36 ;
hence p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) by A2, A3, A25, A23, TOPREAL3:6; :: 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 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:11;
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:11;
A30: width (Gauge (C,(i + 1))) = len (Gauge (C,(i + 1))) by JORDAN8:def 1;
then width (Gauge (C,(i + 1))) >= 4 by JORDAN8:10;
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:12;
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_0:30;
A34: width (Gauge (C,1)) = len (Gauge (C,1)) by JORDAN8:def 1;
then width (Gauge (C,1)) >= 4 by JORDAN8:10;
then A35: 1 <= width (Gauge (C,1)) by XXREAL_0:2;
then A36: Center (Gauge (C,1)) <= len (Gauge (C,1)) by A34, JORDAN1B:12;
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 object ; :: 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:61;
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:24;
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:20, JORDAN1B:12;
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:24;
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:22, JORDAN1B:12;
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:2;
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:36 ;
then a1 `1 = ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),(width (Gauge (C,(i + 1)))))) `1 by A31, A32, A29, GOBOARD5:2;
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:7;
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:44, 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:12, JORDAN1B:29;
then consider n being 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:10;
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:38
.= ((Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n)) `1 by A30, A48, A50, JORDAN1A:36 ;
hence p = (Gauge (C,(i + 1))) * ((Center (Gauge (C,(i + 1)))),n) by A2, A27, A49, A47, TOPREAL3:6; :: thesis: verum

end;

end;