let C be Simple_closed_curve; for n, m being 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 Nat; ( 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)))
; contradiction
A4:
j is_sufficiently_large_for C
by A1, A2, Th28;
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;
consider i1 being 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 left_cell ((Span (C,j)),i1,(Gauge (C,j))) c= Cl (RightComp (Span (C,i)))
ex
i2,
j2 being
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:25;
then consider i5,
j5 being
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 9;
A17:
1
<= i5
by A15, MATRIX_0:32;
A18:
j5 <= width (Gauge (C,j))
by A15, MATRIX_0:32;
A19:
i5 <= len (Gauge (C,j))
by A15, MATRIX_0:32;
A20:
1
<= j5
by A15, MATRIX_0:32;
A21:
i1 in dom (Span (C,j))
by A8, A11, FINSEQ_3:25;
then consider i4,
j4 being
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 9;
A24:
1
<= i4
by A22, MATRIX_0:32;
|.(i4 - i5).| + |.(j4 - j5).| = 1
by A5, A21, A22, A23, A14, A15, A16, GOBOARD1:def 9;
then A25:
( (
|.(i4 - i5).| = 1 &
j4 = j5 ) or (
|.(j4 - j5).| = 1 &
i4 = i5 ) )
by SEQM_3:42;
A26:
1
<= j4
by A22, MATRIX_0:32;
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_0:32;
A29:
i4 <= len (Gauge (C,j))
by A22, MATRIX_0:32;
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, SEQM_3:41;
suppose A30:
(
i4 = i5 &
j4 + 1
= j5 )
;
ex i2, j2 being 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, Th22, Th28;
then
1
+ 1
<= i4
by NAT_1:13;
then A31:
1
<= i4 -' 1
by JORDAN5B:2;
(i4 -' 1) + 1
= i4
by A24, XREAL_1:235;
hence
ex
i2,
j2 being
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:38;
verum suppose A32:
(
i4 + 1
= i5 &
j4 = j5 )
;
ex i2, j2 being 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, Th25, Th28;
then
j4 + 1
<= width (Gauge (C,j))
by NAT_1:13;
hence
ex
i2,
j2 being
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:38;
verum end; suppose A33:
(
i4 = i5 + 1 &
j4 = j5 )
;
ex i2, j2 being 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, Th24, Th28;
then
1
+ 1
<= j5
by NAT_1:13;
then A34:
1
<= j5 -' 1
by JORDAN5B:2;
(j5 -' 1) + 1
= j5
by A20, XREAL_1:235;
hence
ex
i2,
j2 being
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:38;
verum suppose A35:
(
i4 = i5 &
j4 = j5 + 1 )
;
ex i2, j2 being 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, Th23, Th28;
then
i4 + 1
<= len (Gauge (C,j))
by NAT_1:13;
hence
ex
i2,
j2 being
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:38;
verum end;
end; then consider i2,
j2 being
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:21
.=
the
carrier of
(TOP-REAL 2)
by GOBRD14:15
;
assume
not
left_cell (
(Span (C,j)),
i1,
(Gauge (C,j)))
c= Cl (RightComp (Span (C,i)))
;
contradictionthen
not
cell (
(Gauge (C,i)),
i2,
j2)
c= Cl (RightComp (Span (C,i)))
by A38;
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:36;
A45:
Int (left_cell ((Span (C,j)),i1,(Gauge (C,j)))) c= Int (cell ((Gauge (C,i)),i2,j2))
by A38, TOPS_1:19;
A46:
Int (cell ((Gauge (C,i)),i2,j2)) is
convex
by A43, A39, GOBOARD9:17;
Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Span (C,i))) `
by A12, A43, A39, Th33;
then
Int (cell ((Gauge (C,i)),i2,j2)) c= LeftComp (Span (C,i))
by A44, A40, A46, GOBOARD9:4;
then
Int (left_cell ((Span (C,j)),i1,(Gauge (C,j)))) c= LeftComp (Span (C,i))
by A45;
then
Cl (Int (left_cell ((Span (C,j)),i1,(Gauge (C,j))))) c= Cl (LeftComp (Span (C,i)))
by PRE_TOPC:19;
then A47:
left_cell (
(Span (C,j)),
i1,
(Gauge (C,j)))
c= Cl (LeftComp (Span (C,i)))
by A5, A8, A9, JORDAN9:11;
LSeg (
(Span (C,j)),
i1)
c= left_cell (
(Span (C,j)),
i1,
(Gauge (C,j)))
by A5, A8, A9, JORDAN1H:20;
then
LSeg (
(Span (C,j)),
i1)
c= Cl (LeftComp (Span (C,i)))
by A47;
hence
contradiction
by A7, A10;
verum
then A48:
C meets Cl (RightComp (Span (C,i)))
by A4, A8, A9, Th7, XBOOLE_1:63;
A49:
Cl (RightComp (Span (C,i))) = (RightComp (Span (C,i))) \/ (L~ (Span (C,i)))
by GOBRD14:21;
C misses L~ (Span (C,i))
by A1, Th8;
then A50:
C meets RightComp (Span (C,i))
by A48, A49, XBOOLE_1:70;
C meets C
;
then A51:
C meets LeftComp (Span (C,i))
by A1, Th11, 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:10;
then A52:
LeftComp (Span (C,i)) c= D
by XBOOLE_1:7;
C c= LeftComp (Span (C,i))
by A1, Th11;
then A53:
C c= D
by A52;
A54:
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 A50, A53, A54, A51, JORDAN9:1, SPRECT_4:6; verum