let j, i be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st C is connected & i <= j holds
L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( C is connected & i <= j implies L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i))) )
assume that
A1:
C is connected
and
A2:
i <= j
and
A3:
not L~ (Cage (C,j)) c= Cl (RightComp (Cage (C,i)))
; contradiction
A4:
Cage (C,j) is_sequence_on Gauge (C,j)
by A1, JORDAN9:def 1;
A5:
GoB (Cage (C,i)) = Gauge (C,i)
by A1, Th44;
consider p being Point of (TOP-REAL 2) such that
A6:
p in L~ (Cage (C,j))
and
A7:
not p in Cl (RightComp (Cage (C,i)))
by A3;
consider i1 being Nat such that
A8:
1 <= i1
and
A9:
i1 + 1 <= len (Cage (C,j))
and
A10:
p in LSeg ((Cage (C,j)),i1)
by A6, SPPOL_2:13;
A11:
GoB (Cage (C,j)) = Gauge (C,j)
by A1, Th44;
then A12:
right_cell ((Cage (C,j)),i1,(Gauge (C,j))) = right_cell ((Cage (C,j)),i1)
by A8, A9, Th23;
A13:
i1 < len (Cage (C,j))
by A9, NAT_1:13;
now right_cell ((Cage (C,j)),i1) c= Cl (LeftComp (Cage (C,i)))
ex
i2,
j2 being
Nat st
( 1
<= i2 &
i2 + 1
<= len (Gauge (C,i)) & 1
<= j2 &
j2 + 1
<= width (Gauge (C,i)) &
right_cell (
(Cage (C,j)),
i1)
c= cell (
(Gauge (C,i)),
i2,
j2) )
proof
set f =
Cage (
C,
j);
A14:
i1 in dom (Cage (C,j))
by A8, A13, FINSEQ_3:25;
then consider i4,
j4 being
Nat such that A15:
[i4,j4] in Indices (Gauge (C,j))
and A16:
(Cage (C,j)) /. i1 = (Gauge (C,j)) * (
i4,
j4)
by A4, GOBOARD1:def 9;
A17:
1
<= i4
by A15, MATRIX_0:32;
A18:
j4 <= width (Gauge (C,j))
by A15, MATRIX_0:32;
A19:
1
<= j4
by A15, MATRIX_0:32;
A20:
i4 <= len (Gauge (C,j))
by A15, MATRIX_0:32;
1
<= i1 + 1
by NAT_1:11;
then A21:
i1 + 1
in dom (Cage (C,j))
by A9, FINSEQ_3:25;
then consider i5,
j5 being
Nat such that A22:
[i5,j5] in Indices (Gauge (C,j))
and A23:
(Cage (C,j)) /. (i1 + 1) = (Gauge (C,j)) * (
i5,
j5)
by A4, GOBOARD1:def 9;
A24:
1
<= i5
by A22, MATRIX_0:32;
right_cell (
(Cage (C,j)),
i1)
= right_cell (
(Cage (C,j)),
i1)
;
then A25:
( (
i4 = i5 &
j4 + 1
= j5 &
right_cell (
(Cage (C,j)),
i1)
= cell (
(GoB (Cage (C,j))),
i4,
j4) ) or (
i4 + 1
= i5 &
j4 = j5 &
right_cell (
(Cage (C,j)),
i1)
= cell (
(GoB (Cage (C,j))),
i4,
(j4 -' 1)) ) or (
i4 = i5 + 1 &
j4 = j5 &
right_cell (
(Cage (C,j)),
i1)
= cell (
(GoB (Cage (C,j))),
i5,
j5) ) or (
i4 = i5 &
j4 = j5 + 1 &
right_cell (
(Cage (C,j)),
i1)
= cell (
(GoB (Cage (C,j))),
(i4 -' 1),
j5) ) )
by A8, A9, A11, A15, A16, A22, A23, GOBOARD5:def 6;
|.(i4 - i5).| + |.(j4 - j5).| = 1
by A4, A14, A15, A16, A21, A22, A23, GOBOARD1:def 9;
then A26:
( (
|.(i4 - i5).| = 1 &
j4 = j5 ) or (
|.(j4 - j5).| = 1 &
i4 = i5 ) )
by SEQM_3:42;
A27:
j5 <= width (Gauge (C,j))
by A22, MATRIX_0:32;
A28:
i5 <= len (Gauge (C,j))
by A22, MATRIX_0:32;
A29:
1
<= j5
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 A26, 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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )then
i4 < len (Gauge (C,j))
by A1, A8, A9, A15, A16, A22, A23, JORDAN10:1;
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)) &
right_cell (
(Cage (C,j)),
i1)
c= cell (
(Gauge (C,i)),
i2,
j2) )
by A2, A11, A17, A19, A27, A25, A30, Th38;
verum end; suppose A31:
(
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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )then
1
< j4
by A1, A8, A9, A15, A16, A22, A23, JORDAN10:3;
then
1
+ 1
<= j4
by NAT_1:13;
then A32:
1
<= j4 -' 1
by JORDAN5B:2;
(j4 -' 1) + 1
= j4
by A19, 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)) &
right_cell (
(Cage (C,j)),
i1)
c= cell (
(Gauge (C,i)),
i2,
j2) )
by A2, A11, A17, A18, A28, A25, A31, A32, Th38;
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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )then
j5 < width (Gauge (C,j))
by A1, A8, A9, A15, A16, A22, A23, JORDAN10:4;
then
j5 + 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)) &
right_cell (
(Cage (C,j)),
i1)
c= cell (
(Gauge (C,i)),
i2,
j2) )
by A2, A11, A20, A24, A29, A25, A33, Th38;
verum end; suppose A34:
(
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)) & right_cell ((Cage (C,j)),i1) c= cell ((Gauge (C,i)),i2,j2) )then
1
< i4
by A1, A8, A9, A15, A16, A22, A23, JORDAN10:2;
then
1
+ 1
<= i4
by NAT_1:13;
then A35:
1
<= i4 -' 1
by JORDAN5B:2;
(i4 -' 1) + 1
= i4
by A17, 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)) &
right_cell (
(Cage (C,j)),
i1)
c= cell (
(Gauge (C,i)),
i2,
j2) )
by A2, A11, A20, A18, A29, A25, A34, A35, Th38;
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:
right_cell (
(Cage (C,j)),
i1)
c= cell (
(Gauge (C,i)),
i2,
j2)
;
A39:
Int (right_cell ((Cage (C,j)),i1)) c= Int (cell ((Gauge (C,i)),i2,j2))
by A38, TOPS_1:19;
A40:
RightComp (Cage (C,i)) is_a_component_of (L~ (Cage (C,i))) `
by GOBOARD9:def 2;
A41:
(Cl (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i))) =
((L~ (Cage (C,i))) \/ (LeftComp (Cage (C,i)))) \/ (RightComp (Cage (C,i)))
by GOBRD14:22
.=
((L~ (Cage (C,i))) \/ (RightComp (Cage (C,i)))) \/ (LeftComp (Cage (C,i)))
by XBOOLE_1:4
.=
the
carrier of
(TOP-REAL 2)
by GOBRD14:15
;
assume
not
right_cell (
(Cage (C,j)),
i1)
c= Cl (LeftComp (Cage (C,i)))
;
contradictionthen
not
cell (
(Gauge (C,i)),
i2,
j2)
c= Cl (LeftComp (Cage (C,i)))
by A38;
then A42:
cell (
(Gauge (C,i)),
i2,
j2)
meets RightComp (Cage (C,i))
by A41, XBOOLE_1:73;
A43:
(
i2 < len (Gauge (C,i)) &
j2 < width (Gauge (C,i)) )
by A36, A37, NAT_1:13;
then
cell (
(Gauge (C,i)),
i2,
j2)
= Cl (Int (cell ((Gauge (C,i)),i2,j2)))
by GOBRD11:35;
then A44:
Int (cell ((Gauge (C,i)),i2,j2)) meets RightComp (Cage (C,i))
by A42, TSEP_1:36;
A45:
Int (cell ((Gauge (C,i)),i2,j2)) is
convex
by A43, GOBOARD9:17;
Int (cell ((Gauge (C,i)),i2,j2)) c= (L~ (Cage (C,i))) `
by A5, A43, GOBRD12:1;
then
Int (cell ((Gauge (C,i)),i2,j2)) c= RightComp (Cage (C,i))
by A44, A40, A45, GOBOARD9:4;
then
Int (right_cell ((Cage (C,j)),i1)) c= RightComp (Cage (C,i))
by A39;
then
Cl (Int (right_cell ((Cage (C,j)),i1))) c= Cl (RightComp (Cage (C,i)))
by PRE_TOPC:19;
then A46:
right_cell (
(Cage (C,j)),
i1)
c= Cl (RightComp (Cage (C,i)))
by A4, A8, A9, A12, JORDAN9:11;
(
LSeg (
(Cage (C,j)),
i1)
c= right_cell (
(Cage (C,j)),
i1,
(Gauge (C,j))) &
right_cell (
(Cage (C,j)),
i1,
(Gauge (C,j)))
c= right_cell (
(Cage (C,j)),
i1) )
by A4, A8, A9, Th22, GOBRD13:33;
then
LSeg (
(Cage (C,j)),
i1)
c= right_cell (
(Cage (C,j)),
i1)
;
then
LSeg (
(Cage (C,j)),
i1)
c= Cl (RightComp (Cage (C,i)))
by A46;
hence
contradiction
by A7, A10;
verum
then A47:
C meets Cl (LeftComp (Cage (C,i)))
by A1, A8, A9, A12, JORDAN9:31, XBOOLE_1:63;
( Cl (LeftComp (Cage (C,i))) = (LeftComp (Cage (C,i))) \/ (L~ (Cage (C,i))) & C misses L~ (Cage (C,i)) )
by A1, GOBRD14:22, JORDAN10:5;
then A48:
C meets LeftComp (Cage (C,i))
by A47, XBOOLE_1:70;
reconsider D = (L~ (Cage (C,i))) ` as Subset of (TOP-REAL 2) ;
D = (LeftComp (Cage (C,i))) \/ (RightComp (Cage (C,i)))
by GOBRD12:10;
then A49:
RightComp (Cage (C,i)) c= D
by XBOOLE_1:7;
C c= RightComp (Cage (C,i))
by A1, JORDAN10:11;
then A50:
C c= D
by A49;
C meets C
;
then A51:
C meets RightComp (Cage (C,i))
by A1, JORDAN10:11, XBOOLE_1:63;
( LeftComp (Cage (C,i)) is_a_component_of D & RightComp (Cage (C,i)) is_a_component_of D )
by GOBOARD9:def 1, GOBOARD9:def 2;
hence
contradiction
by A1, A48, A50, A51, JORDAN9:1, SPRECT_4:6; verum