let p be Point of (TOP-REAL 2); :: thesis: 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; :: thesis: 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); :: thesis: ( (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 ) ; :: thesis: ( 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) ; :: thesis: 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;

A50: p in LSeg ((f /. (k + 1)),(f /. k)) by A6, A9, A10, A11, TOPREAL1:def 3;

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;

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;

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;

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; :: thesis: 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); :: thesis: ( (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 ) ; :: thesis: ( 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) ; :: thesis: 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 :: thesis: ( 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 ) } )

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;assume
( 1 < j1 & i2 = i1 + 1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A44: now :: thesis: ( 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 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A46: now :: thesis: ( 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 ) } )

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;assume that

A47: 1 = j1 and

A48: i1 = i2 + 1 ; :: thesis: 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; :: thesis: verum

end;A47: 1 = j1 and

A48: i1 = i2 + 1 ; :: thesis: 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; :: thesis: verum

A50: p in LSeg ((f /. (k + 1)),(f /. k)) by A6, A9, A10, A11, TOPREAL1:def 3;

A51: now :: thesis: ( 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 ; :: thesis: ( ((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; :: thesis: verum

end;A52: i1 = i2 and

A53: j1 = j2 + 1 ; :: thesis: ( ((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; :: thesis: verum

A55: now :: thesis: ( 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 ; :: thesis: ( ((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; :: thesis: verum

end;A56: i1 = i2 and

A57: j2 = j1 + 1 ; :: thesis: ( ((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; :: thesis: verum

A58: now :: thesis: ( 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 ) } )

(LSeg (p1,p2)) /\ (LSeg (f,k)) = {p}
by A1, A6, A9, TOPREAL3:19, ZFMISC_1:124;assume that

A59: 1 = i2 and

A60: j1 = j2 + 1 ; :: thesis: 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; :: thesis: verum

end;A59: 1 = i2 and

A60: j1 = j2 + 1 ; :: thesis: 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; :: thesis: verum

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 :: thesis: ( 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 ) } )

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;assume that

A64: 1 = i1 and

A65: j2 = j1 + 1 ; :: thesis: 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; :: thesis: verum

end;A64: 1 = i1 and

A65: j2 = j1 + 1 ; :: thesis: 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; :: thesis: verum

A67: now :: thesis: 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 )

( r in left_cell (f,k,(GoB f)) & not r in L~ f )

let r be Point of (TOP-REAL 2); :: thesis: ( 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))) ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;assume A68: r in Int (left_cell (f,k,(GoB f))) ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

A69: now :: thesis: 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 )

( r in right_cell (f,k,(GoB f)) & not r in L~ f )

let r be Point of (TOP-REAL 2); :: thesis: ( 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))) ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

end;assume A70: r in Int (right_cell (f,k,(GoB f))) ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum

A71: now :: thesis: ( 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 ) } )

( LSeg (f,k) is vertical or LSeg (f,k) is horizontal )
by SPPOL_1:19;assume that

A72: 1 = j1 and

A73: i2 = i1 + 1 ; :: thesis: 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; :: thesis: verum

end;A72: 1 = j1 and

A73: i2 = i1 + 1 ; :: thesis: 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; :: thesis: verum

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 :: thesis: ( j1 = j2 & i2 = i1 + 1 implies ( ((GoB f) * (i1,1)) `1 < p `1 & p `1 < ((GoB f) * ((i1 + 1),1)) `1 ) )

A78:
i2 -' 1 < i2
by A33, JORDAN5B:1;assume that

A76: j1 = j2 and

A77: i2 = i1 + 1 ; :: thesis: ( ((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; :: thesis: verum

end;A76: j1 = j2 and

A77: i2 = i1 + 1 ; :: thesis: ( ((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; :: thesis: verum

A79: now :: thesis: ( 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 ) } )

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;assume
( 1 < i2 & j1 = j2 + 1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A82: now :: thesis: ( j1 = j2 & i1 = i2 + 1 implies ( ((GoB f) * (i2,1)) `1 < p `1 & p `1 < ((GoB f) * ((i2 + 1),1)) `1 ) )

A85:
i1 -' 1 < i1
by A18, JORDAN5B:1;assume that

A83: j1 = j2 and

A84: i1 = i2 + 1 ; :: thesis: ( ((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; :: thesis: verum

end;A83: j1 = j2 and

A84: i1 = i2 + 1 ; :: thesis: ( ((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; :: thesis: verum

A86: now :: thesis: ( 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 ) } )

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;assume
( 1 < i1 & j2 = j1 + 1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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;

end;

suppose A92:
p1 `2 = p2 `2
; :: thesis: 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 )

( 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;

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;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;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 :: thesis: ( j1 = j2 + 1 & 1 < i2 implies rp in Int (right_cell (f,k,(GoB f))) )

assume A96:
( j1 = j2 + 1 & 1 < i2 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A97: now :: thesis: ( j1 = j2 + 1 & 1 = i2 implies rp in Int (right_cell (f,k,(GoB f))) )

Int (left_cell (f,k,(GoB f))) <> {}
by A12, A10, A11, JORDAN9:9;assume A98:
( j1 = j2 + 1 & 1 = i2 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: ( j2 = j1 + 1 & 1 < i1 implies rl in Int (left_cell (f,k,(GoB f))) )

assume A102:
( j2 = j1 + 1 & 1 < i1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A103: now :: thesis: ( j2 = j1 + 1 & 1 = i1 implies rl in Int (left_cell (f,k,(GoB f))) )

A105:
rl `1 = rl9 `1
by EUCLID:52;assume A104:
( j2 = j1 + 1 & 1 = i1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A106: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A108: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A110: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A112: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: 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 )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 )

per cases
( j1 = j2 + 1 or j2 = j1 + 1 )
by A17, A90, A92;

end;

suppose A114:
j1 = j2 + 1
; :: thesis: 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 )

( 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)))

rl in Int (left_cell (f,k,(GoB f)))

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; :: thesis: verum

end;proof
end;

then A115:
( rp in right_cell (f,k,(GoB f)) & not rp in L~ f )
by A69;per cases
( 1 < i2 or 1 = i2 )
by A33, XXREAL_0:1;

end;

rl in Int (left_cell (f,k,(GoB f)))

proof
end;

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; :: thesis: verum

suppose A116:
j2 = j1 + 1
; :: thesis: 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 )

( 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)))

rl in Int (left_cell (f,k,(GoB f)))

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; :: thesis: verum

end;proof
end;

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)))

proof
end;

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; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

suppose A118:
p1 `1 = p2 `1
; :: thesis: 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 )

( 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;

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;

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum

end;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 :: thesis: ( i1 = i2 + 1 & 1 = j1 implies rl in Int (left_cell (f,k,(GoB f))) )

assume A123:
( i1 = i2 + 1 & 1 = j1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A124: now :: thesis: ( i2 = i1 + 1 & j1 < width (GoB f) implies rl in Int (left_cell (f,k,(GoB f))) )

Int (right_cell (f,k,(GoB f))) <> {}
by A12, A10, A11, JORDAN9:9;assume A125:
( i2 = i1 + 1 & j1 < width (GoB f) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: ( i2 = i1 + 1 & 1 < j1 implies rp in Int (right_cell (f,k,(GoB f))) )

assume A129:
( i2 = i1 + 1 & 1 < j1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A130: now :: thesis: ( i2 = i1 + 1 & 1 = j1 implies rp in Int (right_cell (f,k,(GoB f))) )

A132:
rp `2 = rp9 `2
by EUCLID:52;assume A131:
( i2 = i1 + 1 & 1 = j1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A133: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A135: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A137: now :: thesis: ( i1 = i2 + 1 & 1 < j1 implies rl in Int (left_cell (f,k,(GoB f))) )

assume A138:
( i1 = i2 + 1 & 1 < j1 )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

A139: now :: thesis: ( 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) )
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

now :: thesis: 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 )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 )

per cases
( i1 = i2 + 1 or i2 = i1 + 1 )
by A17, A91, A118;

end;

suppose A141:
i1 = i2 + 1
; :: thesis: 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 )

( 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)))

rl in Int (left_cell (f,k,(GoB f)))

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; :: thesis: verum

end;proof
end;

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)))

proof
end;

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; :: thesis: verum

suppose A143:
i2 = i1 + 1
; :: thesis: 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 )

( 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)))

rp in Int (right_cell (f,k,(GoB f)))

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; :: thesis: verum

end;proof
end;

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)))

proof
end;

then
( rp in right_cell (f,k,(GoB f)) & not rp in L~ f )
by A69;per cases
( 1 < j1 or 1 = j1 )
by A24, XXREAL_0:1;

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 ) by A1, A7, A6, A9, A10, A11, A118, A120, A127, A144, Th31; :: thesis: verum

( not C is_a_component_of (L~ f) ` or not p1 in C or not p2 in C ) ; :: thesis: verum