let p be Point of (TOP-REAL 2); for f being non constant standard special_circular_sequence
for p1, p2 being Point of (TOP-REAL 2) st (L~ f) /\ (LSeg (p1,p2)) = {p} & ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & not p1 in L~ f & not p2 in L~ f & rng f misses LSeg (p1,p2) holds
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
let f be non constant standard special_circular_sequence; for p1, p2 being Point of (TOP-REAL 2) st (L~ f) /\ (LSeg (p1,p2)) = {p} & ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & not p1 in L~ f & not p2 in L~ f & rng f misses LSeg (p1,p2) holds
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
let p1, p2 be Point of (TOP-REAL 2); ( (L~ f) /\ (LSeg (p1,p2)) = {p} & ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) & not p1 in L~ f & not p2 in L~ f & rng f misses LSeg (p1,p2) implies for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )
assume that
A1:
(L~ f) /\ (LSeg (p1,p2)) = {p}
and
A2:
( p1 `1 = p2 `1 or p1 `2 = p2 `2 )
; ( p1 in L~ f or p2 in L~ f or not rng f misses LSeg (p1,p2) or for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) )
A3:
p in {p}
by TARSKI:def 1;
then A4:
p in LSeg (p1,p2)
by A1, XBOOLE_0:def 4;
A5:
p in LSeg (p2,p1)
by A1, A3, XBOOLE_0:def 4;
p in L~ f
by A1, A3, XBOOLE_0:def 4;
then consider LS being set such that
A6:
( p in LS & LS in { (LSeg (f,i)) where i is Nat : ( 1 <= i & i + 1 <= len f ) } )
by TARSKI:def 4;
set G = GoB f;
assume that
A7:
( not p1 in L~ f & not p2 in L~ f )
and
A8:
rng f misses LSeg (p1,p2)
; for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
consider k being Nat such that
A9:
LS = LSeg (f,k)
and
A10:
1 <= k
and
A11:
k + 1 <= len f
by A6;
A12:
f is_sequence_on GoB f
by GOBOARD5:def 5;
then consider i1, j1, i2, j2 being Nat such that
A13:
[i1,j1] in Indices (GoB f)
and
A14:
f /. k = (GoB f) * (i1,j1)
and
A15:
[i2,j2] in Indices (GoB f)
and
A16:
f /. (k + 1) = (GoB f) * (i2,j2)
and
A17:
( ( i1 = i2 & j1 + 1 = j2 ) or ( i1 + 1 = i2 & j1 = j2 ) or ( i1 = i2 + 1 & j1 = j2 ) or ( i1 = i2 & j1 = j2 + 1 ) )
by A10, A11, JORDAN8:3;
A18:
1 <= i1
by A13, MATRIX_0:32;
1 <= k + 1
by A10, NAT_1:13;
then A19:
k + 1 in dom f
by A11, FINSEQ_3:25;
then
f . (k + 1) in rng f
by FUNCT_1:3;
then
f /. (k + 1) in rng f
by A19, PARTFUN1:def 6;
then A20:
p <> f /. (k + 1)
by A8, A4, XBOOLE_0:3;
A21:
i2 <= len (GoB f)
by A15, MATRIX_0:32;
then A22:
( i2 = i1 + 1 implies i1 < len (GoB f) )
by NAT_1:13;
then A23:
( j1 = width (GoB f) & i2 = i1 + 1 implies Int (cell ((GoB f),i1,j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(width (GoB f)))) `2 < s ) } )
by A18, GOBOARD6:25;
A24:
1 <= j1
by A13, MATRIX_0:32;
then A25:
( j1 < width (GoB f) & i2 = i1 + 1 implies Int (cell ((GoB f),i1,j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } )
by A18, A22, GOBOARD6:26;
A26:
j2 <= width (GoB f)
by A15, MATRIX_0:32;
then A27:
( j2 = j1 + 1 implies j1 < width (GoB f) )
by NAT_1:13;
then A28:
( i1 = len (GoB f) & j2 = j1 + 1 implies Int (cell ((GoB f),i1,j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((len (GoB f)),1)) `1 < r & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } )
by A24, GOBOARD6:23;
A29:
1 <= j2
by A15, MATRIX_0:32;
A30:
j1 <= width (GoB f)
by A13, MATRIX_0:32;
then A31:
( j1 = j2 + 1 implies j2 < width (GoB f) )
by NAT_1:13;
then A32:
( i2 = len (GoB f) & j1 = j2 + 1 implies Int (cell ((GoB f),i2,j2)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((len (GoB f)),1)) `1 < r & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) } )
by A29, GOBOARD6:23;
A33:
1 <= i2
by A15, MATRIX_0:32;
then A34:
( i2 < len (GoB f) & j1 = j2 + 1 implies Int (cell ((GoB f),i2,j2)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) } )
by A29, A31, GOBOARD6:26;
A35:
i1 <= len (GoB f)
by A13, MATRIX_0:32;
then A36:
( i1 = i2 + 1 implies i2 < len (GoB f) )
by NAT_1:13;
then A37:
( j1 = width (GoB f) & i1 = i2 + 1 implies Int (cell ((GoB f),i2,j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(width (GoB f)))) `2 < s ) } )
by A33, GOBOARD6:25;
k < len f
by A11, NAT_1:13;
then A38:
k in dom f
by A10, FINSEQ_3:25;
then
f . k in rng f
by FUNCT_1:3;
then
f /. k in rng f
by A38, PARTFUN1:def 6;
then A39:
p <> f /. k
by A8, A4, XBOOLE_0:3;
A40:
j1 -' 1 < j1
by A24, JORDAN5B:1;
A41:
now ( 1 < j1 & i2 = i1 + 1 implies Int (cell ((GoB f),i1,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) } )assume
( 1
< j1 &
i2 = i1 + 1 )
;
Int (cell ((GoB f),i1,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) } then A42:
(
i1 < len (GoB f) & 1
<= j1 -' 1 )
by A21, NAT_1:13, NAT_D:49;
( 1
<= i1 &
j1 -' 1
< width (GoB f) )
by A13, A30, A40, MATRIX_0:32, XXREAL_0:2;
hence
Int (cell ((GoB f),i1,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) }
by A42, GOBOARD6:26;
verum end;
A43:
( j1 < width (GoB f) & i1 = i2 + 1 implies Int (cell ((GoB f),i2,j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } )
by A33, A24, A36, GOBOARD6:26;
A44:
now ( 1 < j1 & i1 = i2 + 1 implies Int (cell ((GoB f),i2,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) } )assume
( 1
< j1 &
i1 = i2 + 1 )
;
Int (cell ((GoB f),i2,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) } then A45:
(
i2 < len (GoB f) & 1
<= j1 -' 1 )
by A35, NAT_1:13, NAT_D:49;
( 1
<= i2 &
j1 -' 1
< width (GoB f) )
by A15, A30, A40, MATRIX_0:32, XXREAL_0:2;
hence
Int (cell ((GoB f),i2,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & ((GoB f) * (1,(j1 -' 1))) `2 < s & s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 ) }
by A45, GOBOARD6:26;
verum end;
A46:
now ( 1 = j1 & i1 = i2 + 1 implies Int (cell ((GoB f),i2,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) } )assume that A47:
1
= j1
and A48:
i1 = i2 + 1
;
Int (cell ((GoB f),i2,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) }
Int (cell ((GoB f),i2,0)) = Int (cell ((GoB f),i2,(j1 -' 1)))
by A47, NAT_2:8;
hence
Int (cell ((GoB f),i2,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i2,1)) `1 < r & r < ((GoB f) * ((i2 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) }
by A33, A36, A48, GOBOARD6:24;
verum end;
A49:
( j1 = j2 & i2 = i1 + 1 implies ( Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),i1,j1)) & Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),i1,(j1 -' 1))) ) )
by A12, A10, A11, A13, A14, A15, A16, GOBRD13:23, GOBRD13:24;
A50:
p in LSeg ((f /. (k + 1)),(f /. k))
by A6, A9, A10, A11, TOPREAL1:def 3;
A51:
now ( i1 = i2 & j1 = j2 + 1 implies ( ((GoB f) * (1,j2)) `2 < p `2 & p `2 < ((GoB f) * (1,(j2 + 1))) `2 ) )assume that A52:
i1 = i2
and A53:
j1 = j2 + 1
;
( ((GoB f) * (1,j2)) `2 < p `2 & p `2 < ((GoB f) * (1,(j2 + 1))) `2 )
j2 < j1
by A53, NAT_1:13;
then
(f /. (k + 1)) `2 < (f /. k) `2
by A14, A16, A35, A18, A30, A29, A52, GOBOARD5:4;
then A54:
(
(f /. (k + 1)) `2 < p `2 &
p `2 < (f /. k) `2 )
by A39, A50, A20, TOPREAL6:30;
( 1
<= j2 + 1 &
j2 + 1
<= width (GoB f) )
by A13, A53, MATRIX_0:32;
hence
(
((GoB f) * (1,j2)) `2 < p `2 &
p `2 < ((GoB f) * (1,(j2 + 1))) `2 )
by A14, A16, A35, A18, A26, A29, A52, A53, A54, GOBOARD5:1;
verum end;
A55:
now ( i1 = i2 & j2 = j1 + 1 implies ( ((GoB f) * (1,j1)) `2 < p `2 & p `2 < ((GoB f) * (1,(j1 + 1))) `2 ) )assume that A56:
i1 = i2
and A57:
j2 = j1 + 1
;
( ((GoB f) * (1,j1)) `2 < p `2 & p `2 < ((GoB f) * (1,(j1 + 1))) `2 )
j1 < j2
by A57, NAT_1:13;
then
(f /. k) `2 < (f /. (k + 1)) `2
by A14, A16, A35, A18, A24, A26, A56, GOBOARD5:4;
then
(
(f /. k) `2 < p `2 &
p `2 < (f /. (k + 1)) `2 )
by A39, A50, A20, TOPREAL6:30;
hence
(
((GoB f) * (1,j1)) `2 < p `2 &
p `2 < ((GoB f) * (1,(j1 + 1))) `2 )
by A14, A16, A33, A35, A24, A30, A26, A29, A56, A57, GOBOARD5:1;
verum end;
A58:
now ( 1 = i2 & j1 = j2 + 1 implies Int (cell ((GoB f),(i2 -' 1),j2)) = { |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) } )assume that A59:
1
= i2
and A60:
j1 = j2 + 1
;
Int (cell ((GoB f),(i2 -' 1),j2)) = { |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) }
Int (cell ((GoB f),(i2 -' 1),j2)) = Int (cell ((GoB f),0,j2))
by A59, NAT_2:8;
hence
Int (cell ((GoB f),(i2 -' 1),j2)) = { |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) }
by A29, A31, A60, GOBOARD6:20;
verum end;
(LSeg (p1,p2)) /\ (LSeg (f,k)) = {p}
by A1, A6, A9, TOPREAL3:19, ZFMISC_1:124;
then A61:
(LSeg (p1,p2)) /\ (LSeg ((f /. k),(f /. (k + 1)))) = {p}
by A10, A11, TOPREAL1:def 3;
A62:
( i1 < len (GoB f) & j2 = j1 + 1 implies Int (cell ((GoB f),i1,j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } )
by A18, A24, A27, GOBOARD6:26;
A63:
now ( 1 = i1 & j2 = j1 + 1 implies Int (cell ((GoB f),(i1 -' 1),j1)) = { |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } )assume that A64:
1
= i1
and A65:
j2 = j1 + 1
;
Int (cell ((GoB f),(i1 -' 1),j1)) = { |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) }
Int (cell ((GoB f),(i1 -' 1),j1)) = Int (cell ((GoB f),0,j1))
by A64, NAT_2:8;
hence
Int (cell ((GoB f),(i1 -' 1),j1)) = { |[r,s]| where r, s is Real : ( r < ((GoB f) * (1,1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) }
by A24, A27, A65, GOBOARD6:20;
verum end;
A66:
( i1 = i2 & j1 = j2 + 1 implies ( Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),(i2 -' 1),j2)) & Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),i2,j2)) ) )
by A12, A10, A11, A13, A14, A15, A16, GOBRD13:27, GOBRD13:28;
A67:
now for r being Point of (TOP-REAL 2) st r in Int (left_cell (f,k,(GoB f))) holds
( r in left_cell (f,k,(GoB f)) & not r in L~ f )let r be
Point of
(TOP-REAL 2);
( r in Int (left_cell (f,k,(GoB f))) implies ( r in left_cell (f,k,(GoB f)) & not r in L~ f ) )assume A68:
r in Int (left_cell (f,k,(GoB f)))
;
( r in left_cell (f,k,(GoB f)) & not r in L~ f )
Int (left_cell (f,k,(GoB f))) c= left_cell (
f,
k,
(GoB f))
by TOPS_1:16;
hence
r in left_cell (
f,
k,
(GoB f))
by A68;
not r in L~ f
Int (left_cell (f,k,(GoB f))) misses L~ f
by A12, A10, A11, JORDAN9:15;
hence
not
r in L~ f
by A68, XBOOLE_0:3;
verum end;
A69:
now for r being Point of (TOP-REAL 2) st r in Int (right_cell (f,k,(GoB f))) holds
( r in right_cell (f,k,(GoB f)) & not r in L~ f )let r be
Point of
(TOP-REAL 2);
( r in Int (right_cell (f,k,(GoB f))) implies ( r in right_cell (f,k,(GoB f)) & not r in L~ f ) )assume A70:
r in Int (right_cell (f,k,(GoB f)))
;
( r in right_cell (f,k,(GoB f)) & not r in L~ f )
Int (right_cell (f,k,(GoB f))) c= right_cell (
f,
k,
(GoB f))
by TOPS_1:16;
hence
r in right_cell (
f,
k,
(GoB f))
by A70;
not r in L~ f
Int (right_cell (f,k,(GoB f))) misses L~ f
by A12, A10, A11, JORDAN9:15;
hence
not
r in L~ f
by A70, XBOOLE_0:3;
verum end;
A71:
now ( 1 = j1 & i2 = i1 + 1 implies Int (cell ((GoB f),i1,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) } )assume that A72:
1
= j1
and A73:
i2 = i1 + 1
;
Int (cell ((GoB f),i1,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) }
Int (cell ((GoB f),i1,0)) = Int (cell ((GoB f),i1,(j1 -' 1)))
by A72, NAT_2:8;
hence
Int (cell ((GoB f),i1,(j1 -' 1))) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i1,1)) `1 < r & r < ((GoB f) * ((i1 + 1),1)) `1 & s < ((GoB f) * (1,1)) `2 ) }
by A18, A22, A73, GOBOARD6:24;
verum end;
( LSeg (f,k) is vertical or LSeg (f,k) is horizontal )
by SPPOL_1:19;
then
( LSeg ((f /. k),(f /. (k + 1))) is vertical or LSeg ((f /. k),(f /. (k + 1))) is horizontal )
by A10, A11, TOPREAL1:def 3;
then A74:
( (f /. k) `1 = (f /. (k + 1)) `1 or (f /. k) `2 = (f /. (k + 1)) `2 )
by SPPOL_1:15, SPPOL_1:16;
A75:
now ( j1 = j2 & i2 = i1 + 1 implies ( ((GoB f) * (i1,1)) `1 < p `1 & p `1 < ((GoB f) * ((i1 + 1),1)) `1 ) )assume that A76:
j1 = j2
and A77:
i2 = i1 + 1
;
( ((GoB f) * (i1,1)) `1 < p `1 & p `1 < ((GoB f) * ((i1 + 1),1)) `1 )
i1 < i2
by A77, NAT_1:13;
then
(f /. k) `1 < (f /. (k + 1)) `1
by A14, A16, A21, A18, A26, A29, A76, GOBOARD5:3;
then
(
(f /. k) `1 < p `1 &
p `1 < (f /. (k + 1)) `1 )
by A39, A50, A20, TOPREAL6:29;
hence
(
((GoB f) * (i1,1)) `1 < p `1 &
p `1 < ((GoB f) * ((i1 + 1),1)) `1 )
by A14, A16, A21, A33, A35, A18, A30, A29, A76, A77, GOBOARD5:2;
verum end;
A78:
i2 -' 1 < i2
by A33, JORDAN5B:1;
A79:
now ( 1 < i2 & j1 = j2 + 1 implies Int (cell ((GoB f),(i2 -' 1),j2)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 -' 1),1)) `1 < r & r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) } )assume
( 1
< i2 &
j1 = j2 + 1 )
;
Int (cell ((GoB f),(i2 -' 1),j2)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 -' 1),1)) `1 < r & r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) } then A80:
( 1
<= i2 -' 1 &
j2 < width (GoB f) )
by A30, NAT_1:13, NAT_D:49;
(
i2 -' 1
< len (GoB f) & 1
<= j2 )
by A15, A21, A78, MATRIX_0:32, XXREAL_0:2;
hence
Int (cell ((GoB f),(i2 -' 1),j2)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((i2 -' 1),1)) `1 < r & r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 & ((GoB f) * (1,j2)) `2 < s & s < ((GoB f) * (1,(j2 + 1))) `2 ) }
by A80, GOBOARD6:26;
verum end;
A81:
( j1 = j2 & i1 = i2 + 1 implies ( Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),i2,(j1 -' 1))) & Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),i2,j1)) ) )
by A12, A10, A11, A13, A14, A15, A16, GOBRD13:25, GOBRD13:26;
A82:
now ( j1 = j2 & i1 = i2 + 1 implies ( ((GoB f) * (i2,1)) `1 < p `1 & p `1 < ((GoB f) * ((i2 + 1),1)) `1 ) )assume that A83:
j1 = j2
and A84:
i1 = i2 + 1
;
( ((GoB f) * (i2,1)) `1 < p `1 & p `1 < ((GoB f) * ((i2 + 1),1)) `1 )
i2 < i1
by A84, NAT_1:13;
then
((GoB f) * (i2,j1)) `1 < ((GoB f) * (i1,j1)) `1
by A33, A35, A24, A30, GOBOARD5:3;
then
(
(f /. (k + 1)) `1 < p `1 &
p `1 < (f /. k) `1 )
by A14, A16, A39, A50, A20, A83, TOPREAL6:29;
hence
(
((GoB f) * (i2,1)) `1 < p `1 &
p `1 < ((GoB f) * ((i2 + 1),1)) `1 )
by A14, A16, A21, A33, A35, A18, A26, A29, A83, A84, GOBOARD5:2;
verum end;
A85:
i1 -' 1 < i1
by A18, JORDAN5B:1;
A86:
now ( 1 < i1 & j2 = j1 + 1 implies Int (cell ((GoB f),(i1 -' 1),j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 -' 1),1)) `1 < r & r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } )assume
( 1
< i1 &
j2 = j1 + 1 )
;
Int (cell ((GoB f),(i1 -' 1),j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 -' 1),1)) `1 < r & r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) } then A87:
( 1
<= i1 -' 1 &
j1 < width (GoB f) )
by A26, NAT_1:13, NAT_D:49;
(
i1 -' 1
< len (GoB f) & 1
<= j1 )
by A13, A35, A85, MATRIX_0:32, XXREAL_0:2;
hence
Int (cell ((GoB f),(i1 -' 1),j1)) = { |[r,s]| where r, s is Real : ( ((GoB f) * ((i1 -' 1),1)) `1 < r & r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 & ((GoB f) * (1,j1)) `2 < s & s < ((GoB f) * (1,(j1 + 1))) `2 ) }
by A87, GOBOARD6:26;
verum end;
A88:
( i1 = i2 & j2 = j1 + 1 implies ( Int (left_cell (f,k,(GoB f))) = Int (cell ((GoB f),(i1 -' 1),j1)) & Int (right_cell (f,k,(GoB f))) = Int (cell ((GoB f),i1,j1)) ) )
by A12, A10, A11, A13, A14, A15, A16, GOBRD13:21, GOBRD13:22;
A89:
( p <> p1 & p <> p2 )
by A1, A7, A3, XBOOLE_0:def 4;
then A90:
( p1 `2 = p2 `2 implies i1 = i2 )
by A13, A14, A15, A16, A74, A61, A39, Th29, JORDAN1G:7;
A91:
( p1 `1 = p2 `1 implies j1 = j2 )
by A13, A14, A15, A16, A74, A61, A89, A39, Th29, JORDAN1G:6;
per cases
( p1 `2 = p2 `2 or p1 `1 = p2 `1 )
by A2;
suppose A92:
p1 `2 = p2 `2
;
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
Int (right_cell (f,k,(GoB f))) <> {}
by A12, A10, A11, JORDAN9:9;
then consider rp9 being
object such that A93:
rp9 in Int (right_cell (f,k,(GoB f)))
by XBOOLE_0:def 1;
reconsider rp9 =
rp9 as
Point of
(TOP-REAL 2) by A93;
reconsider rp =
|[(rp9 `1),(p `2)]| as
Point of
(TOP-REAL 2) ;
A94:
p `2 = p1 `2
by A5, A92, GOBOARD7:6;
A95:
now ( j1 = j2 + 1 & 1 < i2 implies rp in Int (right_cell (f,k,(GoB f))) )assume A96:
(
j1 = j2 + 1 & 1
< i2 )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * ((i2 -' 1),1)) `1 < r &
r < ((GoB f) * (((i2 -' 1) + 1),1)) `1 &
((GoB f) * (1,j2)) `2 < s &
s < ((GoB f) * (1,(j2 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A66, A79, A92, A93, Th29, JORDAN1G:7;
then
(
((GoB f) * ((i2 -' 1),1)) `1 < rp9 `1 &
rp9 `1 < ((GoB f) * (((i2 -' 1) + 1),1)) `1 )
by EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A79, A92, A96, Th29, JORDAN1G:7;
verum end; A97:
now ( j1 = j2 + 1 & 1 = i2 implies rp in Int (right_cell (f,k,(GoB f))) )assume A98:
(
j1 = j2 + 1 & 1
= i2 )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
r < ((GoB f) * (1,1)) `1 &
((GoB f) * (1,j2)) `2 < s &
s < ((GoB f) * (1,(j2 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A66, A58, A92, A93, Th29, JORDAN1G:7;
then
rp9 `1 < ((GoB f) * (1,1)) `1
by EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A58, A92, A98, Th29, JORDAN1G:7;
verum end;
Int (left_cell (f,k,(GoB f))) <> {}
by A12, A10, A11, JORDAN9:9;
then consider rl9 being
object such that A99:
rl9 in Int (left_cell (f,k,(GoB f)))
by XBOOLE_0:def 1;
reconsider rl9 =
rl9 as
Point of
(TOP-REAL 2) by A99;
reconsider rl =
|[(rl9 `1),(p `2)]| as
Point of
(TOP-REAL 2) ;
A100:
(
rl `2 = p `2 &
rp `2 = p `2 )
by EUCLID:52;
A101:
now ( j2 = j1 + 1 & 1 < i1 implies rl in Int (left_cell (f,k,(GoB f))) )assume A102:
(
j2 = j1 + 1 & 1
< i1 )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * ((i1 -' 1),1)) `1 < r &
r < ((GoB f) * (((i1 -' 1) + 1),1)) `1 &
((GoB f) * (1,j1)) `2 < s &
s < ((GoB f) * (1,(j1 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A88, A86, A92, A99, Th29, JORDAN1G:7;
then
(
((GoB f) * ((i1 -' 1),1)) `1 < rl9 `1 &
rl9 `1 < ((GoB f) * (((i1 -' 1) + 1),1)) `1 )
by EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A86, A92, A102, Th29, JORDAN1G:7;
verum end; A103:
now ( j2 = j1 + 1 & 1 = i1 implies rl in Int (left_cell (f,k,(GoB f))) )assume A104:
(
j2 = j1 + 1 & 1
= i1 )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
r < ((GoB f) * (1,1)) `1 &
((GoB f) * (1,j1)) `2 < s &
s < ((GoB f) * (1,(j1 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A88, A63, A92, A99, Th29, JORDAN1G:7;
then
rl9 `1 < ((GoB f) * (1,1)) `1
by EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A63, A92, A104, Th29, JORDAN1G:7;
verum end; A105:
rl `1 = rl9 `1
by EUCLID:52;
A106:
now ( j1 = j2 + 1 & i2 = len (GoB f) implies rl in Int (left_cell (f,k,(GoB f))) )assume A107:
(
j1 = j2 + 1 &
i2 = len (GoB f) )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * ((len (GoB f)),1)) `1 < r &
((GoB f) * (1,j2)) `2 < s &
s < ((GoB f) * (1,(j2 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A66, A32, A92, A99, Th29, JORDAN1G:7;
then
((GoB f) * ((len (GoB f)),1)) `1 < rl `1
by A105, EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A32, A92, A105, A107, Th29, JORDAN1G:7;
verum end; A108:
now ( j2 = j1 + 1 & i1 = len (GoB f) implies rp in Int (right_cell (f,k,(GoB f))) )assume A109:
(
j2 = j1 + 1 &
i1 = len (GoB f) )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * ((len (GoB f)),1)) `1 < r &
((GoB f) * (1,j1)) `2 < s &
s < ((GoB f) * (1,(j1 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A88, A28, A92, A93, Th29, JORDAN1G:7;
then
((GoB f) * ((len (GoB f)),1)) `1 < rp9 `1
by EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A28, A92, A109, Th29, JORDAN1G:7;
verum end; A110:
now ( j2 = j1 + 1 & i1 < len (GoB f) implies rp in Int (right_cell (f,k,(GoB f))) )assume A111:
(
j2 = j1 + 1 &
i1 < len (GoB f) )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * (i1,1)) `1 < r &
r < ((GoB f) * ((i1 + 1),1)) `1 &
((GoB f) * (1,j1)) `2 < s &
s < ((GoB f) * (1,(j1 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A88, A62, A92, A93, Th29, JORDAN1G:7;
then
(
((GoB f) * (i1,1)) `1 < rp9 `1 &
rp9 `1 < ((GoB f) * ((i1 + 1),1)) `1 )
by EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A55, A88, A62, A92, A111, Th29, JORDAN1G:7;
verum end; A112:
now ( j1 = j2 + 1 & i2 < len (GoB f) implies rl in Int (left_cell (f,k,(GoB f))) )assume A113:
(
j1 = j2 + 1 &
i2 < len (GoB f) )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * (i2,1)) `1 < r &
r < ((GoB f) * ((i2 + 1),1)) `1 &
((GoB f) * (1,j2)) `2 < s &
s < ((GoB f) * (1,(j2 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A66, A34, A92, A99, Th29, JORDAN1G:7;
then
(
((GoB f) * (i2,1)) `1 < rl `1 &
rl `1 < ((GoB f) * ((i2 + 1),1)) `1 )
by A105, EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A51, A66, A34, A92, A105, A113, Th29, JORDAN1G:7;
verum end; now for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )per cases
( j1 = j2 + 1 or j2 = j1 + 1 )
by A17, A90, A92;
suppose A114:
j1 = j2 + 1
;
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
rp in Int (right_cell (f,k,(GoB f)))
then A115:
(
rp in right_cell (
f,
k,
(GoB f)) & not
rp in L~ f )
by A69;
rl in Int (left_cell (f,k,(GoB f)))
then
(
rl in left_cell (
f,
k,
(GoB f)) & not
rl in L~ f )
by A67;
hence
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ f) ` or not
p1 in C or not
p2 in C )
by A1, A7, A6, A9, A10, A11, A92, A94, A100, A115, Th31;
verum end; suppose A116:
j2 = j1 + 1
;
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
rp in Int (right_cell (f,k,(GoB f)))
then A117:
(
rp in right_cell (
f,
k,
(GoB f)) & not
rp in L~ f )
by A69;
rl in Int (left_cell (f,k,(GoB f)))
then
(
rl in left_cell (
f,
k,
(GoB f)) & not
rl in L~ f )
by A67;
hence
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ f) ` or not
p1 in C or not
p2 in C )
by A1, A7, A6, A9, A10, A11, A92, A94, A100, A117, Th31;
verum end; hence
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ f) ` or not
p1 in C or not
p2 in C )
;
verum end; suppose A118:
p1 `1 = p2 `1
;
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
Int (left_cell (f,k,(GoB f))) <> {}
by A12, A10, A11, JORDAN9:9;
then consider rl9 being
object such that A119:
rl9 in Int (left_cell (f,k,(GoB f)))
by XBOOLE_0:def 1;
reconsider rl9 =
rl9 as
Point of
(TOP-REAL 2) by A119;
reconsider rl =
|[(p `1),(rl9 `2)]| as
Point of
(TOP-REAL 2) ;
A120:
p `1 = p1 `1
by A5, A118, GOBOARD7:5;
A121:
rl `2 = rl9 `2
by EUCLID:52;
A122:
now ( i1 = i2 + 1 & 1 = j1 implies rl in Int (left_cell (f,k,(GoB f))) )assume A123:
(
i1 = i2 + 1 & 1
= j1 )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * (i2,1)) `1 < r &
r < ((GoB f) * ((i2 + 1),1)) `1 &
s < ((GoB f) * (1,1)) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A81, A46, A118, A119, Th29, JORDAN1G:6;
then
rl `2 < ((GoB f) * (1,1)) `2
by A121, EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A46, A118, A121, A123, Th29, JORDAN1G:6;
verum end; A124:
now ( i2 = i1 + 1 & j1 < width (GoB f) implies rl in Int (left_cell (f,k,(GoB f))) )assume A125:
(
i2 = i1 + 1 &
j1 < width (GoB f) )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * (i1,1)) `1 < r &
r < ((GoB f) * ((i1 + 1),1)) `1 &
((GoB f) * (1,j1)) `2 < s &
s < ((GoB f) * (1,(j1 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A49, A25, A118, A119, Th29, JORDAN1G:6;
then
(
((GoB f) * (1,j1)) `2 < rl `2 &
rl `2 < ((GoB f) * (1,(j1 + 1))) `2 )
by A121, EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A25, A118, A121, A125, Th29, JORDAN1G:6;
verum end;
Int (right_cell (f,k,(GoB f))) <> {}
by A12, A10, A11, JORDAN9:9;
then consider rp9 being
object such that A126:
rp9 in Int (right_cell (f,k,(GoB f)))
by XBOOLE_0:def 1;
reconsider rp9 =
rp9 as
Point of
(TOP-REAL 2) by A126;
reconsider rp =
|[(p `1),(rp9 `2)]| as
Point of
(TOP-REAL 2) ;
A127:
(
rl `1 = p `1 &
rp `1 = p `1 )
by EUCLID:52;
A128:
now ( i2 = i1 + 1 & 1 < j1 implies rp in Int (right_cell (f,k,(GoB f))) )assume A129:
(
i2 = i1 + 1 & 1
< j1 )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * (i1,1)) `1 < r &
r < ((GoB f) * ((i1 + 1),1)) `1 &
((GoB f) * (1,(j1 -' 1))) `2 < s &
s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A49, A41, A118, A126, Th29, JORDAN1G:6;
then
(
((GoB f) * (1,(j1 -' 1))) `2 < rp9 `2 &
rp9 `2 < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )
by EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A41, A118, A129, Th29, JORDAN1G:6;
verum end; A130:
now ( i2 = i1 + 1 & 1 = j1 implies rp in Int (right_cell (f,k,(GoB f))) )assume A131:
(
i2 = i1 + 1 & 1
= j1 )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * (i1,1)) `1 < r &
r < ((GoB f) * ((i1 + 1),1)) `1 &
s < ((GoB f) * (1,1)) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A49, A71, A118, A126, Th29, JORDAN1G:6;
then
rp9 `2 < ((GoB f) * (1,1)) `2
by EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A71, A118, A131, Th29, JORDAN1G:6;
verum end; A132:
rp `2 = rp9 `2
by EUCLID:52;
A133:
now ( i1 = i2 + 1 & j1 = width (GoB f) implies rp in Int (right_cell (f,k,(GoB f))) )assume A134:
(
i1 = i2 + 1 &
j1 = width (GoB f) )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * (i2,1)) `1 < r &
r < ((GoB f) * ((i2 + 1),1)) `1 &
((GoB f) * (1,(width (GoB f)))) `2 < s )
by A13, A14, A15, A16, A74, A61, A89, A39, A81, A37, A118, A126, Th29, JORDAN1G:6;
then
((GoB f) * (1,(width (GoB f)))) `2 < rp `2
by A132, EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A37, A118, A132, A134, Th29, JORDAN1G:6;
verum end; A135:
now ( i2 = i1 + 1 & j1 = width (GoB f) implies rl in Int (left_cell (f,k,(GoB f))) )assume A136:
(
i2 = i1 + 1 &
j1 = width (GoB f) )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * (i1,1)) `1 < r &
r < ((GoB f) * ((i1 + 1),1)) `1 &
((GoB f) * (1,(width (GoB f)))) `2 < s )
by A13, A14, A15, A16, A74, A61, A89, A39, A49, A23, A118, A119, Th29, JORDAN1G:6;
then
((GoB f) * (1,(width (GoB f)))) `2 < rl9 `2
by EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A75, A49, A23, A118, A136, Th29, JORDAN1G:6;
verum end; A137:
now ( i1 = i2 + 1 & 1 < j1 implies rl in Int (left_cell (f,k,(GoB f))) )assume A138:
(
i1 = i2 + 1 & 1
< j1 )
;
rl in Int (left_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rl9 = |[r,s]| &
((GoB f) * (i2,1)) `1 < r &
r < ((GoB f) * ((i2 + 1),1)) `1 &
((GoB f) * (1,(j1 -' 1))) `2 < s &
s < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A81, A44, A118, A119, Th29, JORDAN1G:6;
then
(
((GoB f) * (1,(j1 -' 1))) `2 < rl9 `2 &
rl9 `2 < ((GoB f) * (1,((j1 -' 1) + 1))) `2 )
by EUCLID:52;
hence
rl in Int (left_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A44, A118, A138, Th29, JORDAN1G:6;
verum end; A139:
now ( i1 = i2 + 1 & j1 < width (GoB f) implies rp in Int (right_cell (f,k,(GoB f))) )assume A140:
(
i1 = i2 + 1 &
j1 < width (GoB f) )
;
rp in Int (right_cell (f,k,(GoB f)))then
ex
r,
s being
Real st
(
rp9 = |[r,s]| &
((GoB f) * (i2,1)) `1 < r &
r < ((GoB f) * ((i2 + 1),1)) `1 &
((GoB f) * (1,j1)) `2 < s &
s < ((GoB f) * (1,(j1 + 1))) `2 )
by A13, A14, A15, A16, A74, A61, A89, A39, A81, A43, A118, A126, Th29, JORDAN1G:6;
then
(
((GoB f) * (1,j1)) `2 < rp `2 &
rp `2 < ((GoB f) * (1,(j1 + 1))) `2 )
by A132, EUCLID:52;
hence
rp in Int (right_cell (f,k,(GoB f)))
by A13, A14, A15, A16, A74, A61, A89, A39, A82, A81, A43, A118, A132, A140, Th29, JORDAN1G:6;
verum end; now for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )per cases
( i1 = i2 + 1 or i2 = i1 + 1 )
by A17, A91, A118;
suppose A141:
i1 = i2 + 1
;
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
rp in Int (right_cell (f,k,(GoB f)))
then A142:
(
rp in right_cell (
f,
k,
(GoB f)) & not
rp in L~ f )
by A69;
rl in Int (left_cell (f,k,(GoB f)))
then
(
rl in left_cell (
f,
k,
(GoB f)) & not
rl in L~ f )
by A67;
hence
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ f) ` or not
p1 in C or not
p2 in C )
by A1, A7, A6, A9, A10, A11, A118, A120, A127, A142, Th31;
verum end; suppose A143:
i2 = i1 + 1
;
for C being Subset of (TOP-REAL 2) holds
( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C )
rl in Int (left_cell (f,k,(GoB f)))
then A144:
(
rl in left_cell (
f,
k,
(GoB f)) & not
rl in L~ f )
by A67;
rp in Int (right_cell (f,k,(GoB f)))
then
(
rp in right_cell (
f,
k,
(GoB f)) & not
rp in L~ f )
by A69;
hence
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ f) ` or not
p1 in C or not
p2 in C )
by A1, A7, A6, A9, A10, A11, A118, A120, A127, A144, Th31;
verum end; hence
for
C being
Subset of
(TOP-REAL 2) holds
( not
C is_a_component_of (L~ f) ` or not
p1 in C or not
p2 in C )
;
verum end;