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;
A6:
Span C,i is_sequence_on Gauge C,i
by A1, JORDAN13:def 1;
consider p being Point of (TOP-REAL 2) such that
A7:
p in L~ (Span C,j)
and
A8:
not p in Cl (LeftComp (Span C,i))
by A3, SUBSET_1:7;
reconsider D = (L~ (Span C,i)) ` as Subset of (TOP-REAL 2) ;
consider i1 being Element of NAT such that
A9:
1 <= i1
and
A10:
i1 + 1 <= len (Span C,j)
and
A11:
p in LSeg (Span C,j),i1
by A7, SPPOL_2:13;
A12:
i1 < len (Span C,j)
by A10, NAT_1:13;
set f = Span C,j;
set G = Gauge C,j;
A13:
now assume A14:
not
left_cell (Span C,j),
i1,
(Gauge C,j) c= Cl (RightComp (Span C,i))
;
:: thesis: contradiction
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
A15:
i1 in dom (Span C,j)
by A9, A12, FINSEQ_3:27;
then consider i4,
j4 being
Element of
NAT such that A16:
[i4,j4] in Indices (Gauge C,j)
and A17:
(Span C,j) /. i1 = (Gauge C,j) * i4,
j4
by A5, GOBOARD1:def 11;
A18:
( 1
<= i4 &
i4 <= len (Gauge C,j) )
by A16, MATRIX_1:39;
A19:
( 1
<= j4 &
j4 <= width (Gauge C,j) )
by A16, MATRIX_1:39;
A20:
1
<= i1 + 1
by NAT_1:11;
then A21:
i1 + 1
in dom (Span C,j)
by A10, FINSEQ_3:27;
then consider i5,
j5 being
Element of
NAT such that A22:
[i5,j5] in Indices (Gauge C,j)
and A23:
(Span C,j) /. (i1 + 1) = (Gauge C,j) * i5,
j5
by A5, GOBOARD1:def 11;
A24:
( 1
<= i5 &
i5 <= len (Gauge C,j) )
by A22, MATRIX_1:39;
A25:
( 1
<= j5 &
j5 <= width (Gauge C,j) )
by A22, MATRIX_1:39;
left_cell (Span C,j),
i1,
(Gauge C,j) = left_cell (Span C,j),
i1,
(Gauge C,j)
;
then A26:
( (
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, A9, A10, A16, A17, A22, A23, GOBRD13:def 3;
(abs (i4 - i5)) + (abs (j4 - j5)) = 1
by A5, A15, A16, A17, A21, A22, A23, GOBOARD1:def 11;
then A27:
( (
abs (i4 - i5) = 1 &
j4 = j5 ) or (
abs (j4 - j5) = 1 &
i4 = i5 ) )
by GOBOARD1:2;
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 A27, GOBOARD1:1;
suppose A28:
(
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 )A29:
(i4 -' 1) + 1
= i4
by A18, XREAL_1:237;
1
< i4
by A1, A2, A9, A12, A16, A17, Th23, Th29;
then
1
+ 1
<= i4
by NAT_1:13;
then
1
<= i4 -' 1
by JORDAN5B:2;
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, A18, A19, A25, A26, A28, A29, JORDAN1H:44;
:: thesis: verum end; suppose A30:
(
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, A9, A12, A16, A17, 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, A18, A19, A24, A26, A30, JORDAN1H:44;
:: thesis: verum end; suppose A31:
(
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 )A32:
(j5 -' 1) + 1
= j5
by A25, XREAL_1:237;
1
< j5
by A1, A2, A10, A20, A22, A23, Th25, Th29;
then
1
+ 1
<= j5
by NAT_1:13;
then
1
<= j5 -' 1
by JORDAN5B:2;
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, A18, A24, A25, A26, A31, A32, JORDAN1H:44;
:: thesis: verum end; suppose A33:
(
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, A9, A12, A16, A17, 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, A18, A19, A25, A26, A33, JORDAN1H:44;
:: thesis: verum end;
end; then consider i2,
j2 being
Element of
NAT such that A34:
( 1
<= i2 &
i2 + 1
<= len (Gauge C,i) )
and A35:
( 1
<= j2 &
j2 + 1
<= width (Gauge C,i) )
and A36:
left_cell (Span C,j),
i1,
(Gauge C,j) c= cell (Gauge C,i),
i2,
j2
;
A37:
i2 < len (Gauge C,i)
by A34, NAT_1:13;
A38:
j2 < width (Gauge C,i)
by A35, NAT_1:13;
A39:
not
cell (Gauge C,i),
i2,
j2 c= Cl (RightComp (Span C,i))
by A14, A36, XBOOLE_1:1;
(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
;
then A40:
cell (Gauge C,i),
i2,
j2 meets LeftComp (Span C,i)
by A39, XBOOLE_1:73;
cell (Gauge C,i),
i2,
j2 = Cl (Int (cell (Gauge C,i),i2,j2))
by A37, A38, GOBRD11:35;
then A41:
Int (cell (Gauge C,i),i2,j2) meets LeftComp (Span C,i)
by A40, TSEP_1:40;
A42:
Int (cell (Gauge C,i),i2,j2) c= (L~ (Span C,i)) `
by A6, A37, A38, Th34;
LeftComp (Span C,i) is_a_component_of (L~ (Span C,i)) `
by GOBOARD9:def 1;
then A43:
Int (cell (Gauge C,i),i2,j2) c= LeftComp (Span C,i)
by A37, A38, A41, A42, GOBOARD9:6, GOBOARD9:21;
Int (left_cell (Span C,j),i1,(Gauge C,j)) c= Int (cell (Gauge C,i),i2,j2)
by A36, TOPS_1:48;
then
Int (left_cell (Span C,j),i1,(Gauge C,j)) c= LeftComp (Span C,i)
by A43, 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 A44:
left_cell (Span C,j),
i1,
(Gauge C,j) c= Cl (LeftComp (Span C,i))
by A5, A9, A10, JORDAN9:13;
LSeg (Span C,j),
i1 c= left_cell (Span C,j),
i1,
(Gauge C,j)
by A5, A9, A10, JORDAN1H:26;
then
LSeg (Span C,j),
i1 c= Cl (LeftComp (Span C,i))
by A44, XBOOLE_1:1;
hence
contradiction
by A8, A11;
:: thesis: verum end;
A45:
C c= LeftComp (Span C,i)
by A1, Th12;
left_cell (Span C,j),i1,(Gauge C,j) meets C
by A4, A9, A10, Th8;
then A46:
C meets Cl (RightComp (Span C,i))
by A13, XBOOLE_1:63;
A47:
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 A48:
C meets RightComp (Span C,i)
by A46, A47, XBOOLE_1:70;
A49:
RightComp (Span C,i) is_a_component_of D
by GOBOARD9:def 2;
D = (RightComp (Span C,i)) \/ (LeftComp (Span C,i))
by GOBRD12:11;
then
LeftComp (Span C,i) c= D
by XBOOLE_1:7;
then A50:
C c= D
by A45, XBOOLE_1:1;
A51:
LeftComp (Span C,i) is_a_component_of D
by GOBOARD9:def 1;
C meets C
;
then
C meets LeftComp (Span C,i)
by A1, Th12, XBOOLE_1:63;
hence
contradiction
by A48, A49, A50, A51, JORDAN9:3, SPRECT_4:7; :: thesis: verum