let C be Simple_closed_curve; :: thesis: for n, m being Element of NAT st n is_sufficiently_large_for C & n <= m holds
L~ (Span C,m) c= Cl (LeftComp (Span C,n))
let i, j be Element of NAT ; :: thesis: ( i is_sufficiently_large_for C & i <= j implies L~ (Span C,j) c= Cl (LeftComp (Span C,i)) )
assume that
A1: i is_sufficiently_large_for C and
A2: i <= j and
A3: not L~ (Span C,j) c= Cl (LeftComp (Span C,i)) ; :: thesis: contradiction
A4: j is_sufficiently_large_for C by A1, A2, Th29;
then A5: Span C,j is_sequence_on Gauge C,j by JORDAN13:def 1;
set G = Gauge C,j;
set f = Span C,j;
consider p being Point of (TOP-REAL 2) such that
A6: p in L~ (Span C,j) and
A7: not p in Cl (LeftComp (Span C,i)) by A3, SUBSET_1:7;
consider i1 being Element of NAT such that
A8: 1 <= i1 and
A9: i1 + 1 <= len (Span C,j) and
A10: p in LSeg (Span C,j),i1 by A6, SPPOL_2:13;
A11: i1 < len (Span C,j) by A9, NAT_1:13;
A12: Span C,i is_sequence_on Gauge C,i by A1, JORDAN13:def 1;

now

ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 )

proof

A13: 1 <= i1 + 1 by NAT_1:11;
then A14: i1 + 1 in dom (Span C,j) by A9, FINSEQ_3:27;
then consider i5, j5 being Element of NAT such that
A15: [i5,j5] in Indices (Gauge C,j) and
A16: (Span C,j) /. (i1 + 1) = (Gauge C,j) * i5,j5 by A5, GOBOARD1:def 11;
A17: 1 <= i5 by A15, MATRIX_1:39;
A18: j5 <= width (Gauge C,j) by A15, MATRIX_1:39;
A19: i5 <= len (Gauge C,j) by A15, MATRIX_1:39;
A20: 1 <= j5 by A15, MATRIX_1:39;
A21: i1 in dom (Span C,j) by A8, A11, FINSEQ_3:27;
then consider i4, j4 being Element of NAT such that
A22: [i4,j4] in Indices (Gauge C,j) and
A23: (Span C,j) /. i1 = (Gauge C,j) * i4,j4 by A5, GOBOARD1:def 11;
A24: 1 <= i4 by A22, MATRIX_1:39;
(abs (i4 - i5)) + (abs (j4 - j5)) = 1 by A5, A21, A22, A23, A14, A15, A16, GOBOARD1:def 11;
then A25: ( ( abs (i4 - i5) = 1 & j4 = j5 ) or ( abs (j4 - j5) = 1 & i4 = i5 ) ) by GOBOARD1:2;
A26: 1 <= j4 by A22, MATRIX_1:39;
left_cell (Span C,j),i1,(Gauge C,j) = left_cell (Span C,j),i1,(Gauge C,j) ;
then A27: ( ( i4 = i5 & j4 + 1 = j5 & left_cell (Span C,j),i1,(Gauge C,j) = cell (Gauge C,j),(i4 -' 1),j4 ) or ( i4 + 1 = i5 & j4 = j5 & left_cell (Span C,j),i1,(Gauge C,j) = cell (Gauge C,j),i4,j4 ) or ( i4 = i5 + 1 & j4 = j5 & left_cell (Span C,j),i1,(Gauge C,j) = cell (Gauge C,j),i5,(j5 -' 1) ) or ( i4 = i5 & j4 = j5 + 1 & left_cell (Span C,j),i1,(Gauge C,j) = cell (Gauge C,j),i4,j5 ) ) by A5, A8, A9, A22, A23, A15, A16, GOBRD13:def 3;
A28: j4 <= width (Gauge C,j) by A22, MATRIX_1:39;
A29: i4 <= len (Gauge C,j) by A22, MATRIX_1:39;

per cases ( ( i4 = i5 & j4 + 1 = j5 ) or ( i4 + 1 = i5 & j4 = j5 ) or ( i4 = i5 + 1 & j4 = j5 ) or ( i4 = i5 & j4 = j5 + 1 ) ) by A25, GOBOARD1:1;

suppose A30: ( i4 = i5 & j4 + 1 = j5 ) ; :: thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 )

1 < i4 by A1, A2, A8, A11, A22, A23, Th23, Th29;
then 1 + 1 <= i4 by NAT_1:13;
then A31: 1 <= i4 -' 1 by JORDAN5B:2;
(i4 -' 1) + 1 = i4 by A24, XREAL_1:237;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 ) by A2, A29, A26, A18, A27, A30, A31, JORDAN1H:44; :: thesis: verum

end;

suppose A32: ( i4 + 1 = i5 & j4 = j5 ) ; :: thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 )

j4 < width (Gauge C,j) by A1, A2, A8, A11, A22, A23, Th26, Th29;
then j4 + 1 <= width (Gauge C,j) by NAT_1:13;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 ) by A2, A24, A26, A19, A27, A32, JORDAN1H:44; :: thesis: verum

end;

suppose A33: ( i4 = i5 + 1 & j4 = j5 ) ; :: thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 )

1 < j5 by A1, A2, A9, A13, A15, A16, Th25, Th29;
then 1 + 1 <= j5 by NAT_1:13;
then A34: 1 <= j5 -' 1 by JORDAN5B:2;
(j5 -' 1) + 1 = j5 by A20, XREAL_1:237;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 ) by A2, A29, A17, A18, A27, A33, A34, JORDAN1H:44; :: thesis: verum

end;

suppose A35: ( i4 = i5 & j4 = j5 + 1 ) ; :: thesis: ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 )

i4 < len (Gauge C,j) by A1, A2, A8, A11, A22, A23, Th24, Th29;
then i4 + 1 <= len (Gauge C,j) by NAT_1:13;
hence ex i2, j2 being Element of NAT st
( 1 <= i2 & i2 + 1 <= len (Gauge C,i) & 1 <= j2 & j2 + 1 <= width (Gauge C,i) & left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 ) by A2, A24, A28, A20, A27, A35, JORDAN1H:44; :: thesis: verum

end;

end;

end;

then consider i2, j2 being Element of NAT such that
1 <= i2 and
A36: i2 + 1 <= len (Gauge C,i) and
1 <= j2 and
A37: j2 + 1 <= width (Gauge C,i) and
A38: left_cell (Span C,j),i1,(Gauge C,j) c= cell (Gauge C,i),i2,j2 ;
A39: j2 < width (Gauge C,i) by A37, NAT_1:13;
A40: LeftComp (Span C,i) is_a_component_of (L~ (Span C,i)) ` by GOBOARD9:def 1;
A41: (Cl (RightComp (Span C,i))) \/ (LeftComp (Span C,i)) = ((L~ (Span C,i)) \/ (RightComp (Span C,i))) \/ (LeftComp (Span C,i)) by GOBRD14:31
.= the carrier of (TOP-REAL 2) by GOBRD14:25 ;
assume not left_cell (Span C,j),i1,(Gauge C,j) c= Cl (RightComp (Span C,i)) ; :: thesis: contradiction
then not cell (Gauge C,i),i2,j2 c= Cl (RightComp (Span C,i)) by A38, XBOOLE_1:1;
then A42: cell (Gauge C,i),i2,j2 meets LeftComp (Span C,i) by A41, XBOOLE_1:73;
A43: i2 < len (Gauge C,i) by A36, NAT_1:13;
then cell (Gauge C,i),i2,j2 = Cl (Int (cell (Gauge C,i),i2,j2)) by A39, GOBRD11:35;
then A44: Int (cell (Gauge C,i),i2,j2) meets LeftComp (Span C,i) by A42, TSEP_1:40;
A45: Int (left_cell (Span C,j),i1,(Gauge C,j)) c= Int (cell (Gauge C,i),i2,j2) by A38, TOPS_1:48;
Int (cell (Gauge C,i),i2,j2) c= (L~ (Span C,i)) ` by A12, A43, A39, Th34;
then Int (cell (Gauge C,i),i2,j2) c= LeftComp (Span C,i) by A43, A39, A44, A40, GOBOARD9:6, GOBOARD9:21;
then Int (left_cell (Span C,j),i1,(Gauge C,j)) c= LeftComp (Span C,i) by A45, XBOOLE_1:1;
then Cl (Int (left_cell (Span C,j),i1,(Gauge C,j))) c= Cl (LeftComp (Span C,i)) by PRE_TOPC:49;
then A46: left_cell (Span C,j),i1,(Gauge C,j) c= Cl (LeftComp (Span C,i)) by A5, A8, A9, JORDAN9:13;
LSeg (Span C,j),i1 c= left_cell (Span C,j),i1,(Gauge C,j) by A5, A8, A9, JORDAN1H:26;
then LSeg (Span C,j),i1 c= Cl (LeftComp (Span C,i)) by A46, XBOOLE_1:1;
hence contradiction by A7, A10; :: thesis: verum

end;

then A47: C meets Cl (RightComp (Span C,i)) by A4, A8, A9, Th8, XBOOLE_1:63;
A48: Cl (RightComp (Span C,i)) = (RightComp (Span C,i)) \/ (L~ (Span C,i)) by GOBRD14:31;
C misses L~ (Span C,i) by A1, Th9;
then A49: C meets RightComp (Span C,i) by A47, A48, XBOOLE_1:70;
C meets C ;
then A50: C meets LeftComp (Span C,i) by A1, Th12, XBOOLE_1:63;
reconsider D = (L~ (Span C,i)) ` as Subset of (TOP-REAL 2) ;
D = (RightComp (Span C,i)) \/ (LeftComp (Span C,i)) by GOBRD12:11;
then A51: LeftComp (Span C,i) c= D by XBOOLE_1:7;
C c= LeftComp (Span C,i) by A1, Th12;
then A52: C c= D by A51, XBOOLE_1:1;
A53: LeftComp (Span C,i) is_a_component_of D by GOBOARD9:def 1;
RightComp (Span C,i) is_a_component_of D by GOBOARD9:def 2;
hence contradiction by A49, A52, A53, A50, JORDAN9:3, SPRECT_4:7; :: thesis: verum