let p be Point of (TOP-REAL 2); :: thesis:
let f be non constant standard special_circular_sequence; :: thesis:
let p1, p2 be Point of (TOP-REAL 2); :: thesis:
assume that
A1: (L~ f) /\ (LSeg (p1,p2)) = {p} and
A2: ( p1 `1 = p2 `1 or p1 `2 = p2 `2 ) ; :: thesis:
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:
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:

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

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

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

end;

A46: now :: thesis:

assume that
A47: 1 = j1 and
A48: i1 = i2 + 1 ; :: thesis:
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:

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

assume that
A52: i1 = i2 and
A53: j1 = j2 + 1 ; :: thesis:
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:

end;

A55: now :: thesis:

assume that
A56: i1 = i2 and
A57: j2 = j1 + 1 ; :: thesis:
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:

end;

A58: now :: thesis:

assume that
A59: 1 = i2 and
A60: j1 = j2 + 1 ; :: thesis:
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:

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

assume that
A64: 1 = i1 and
A65: j2 = j1 + 1 ; :: thesis:
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:

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

let r be Point of (TOP-REAL 2); :: thesis:
assume A68: r in Int (left_cell (f,k,(GoB f))) ; :: thesis:
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:
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:

end;

A69: now :: thesis:

let r be Point of (TOP-REAL 2); :: thesis:
assume A70: r in Int (right_cell (f,k,(GoB f))) ; :: thesis:
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:
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:

end;

A71: now :: thesis:

assume that
A72: 1 = j1 and
A73: i2 = i1 + 1 ; :: thesis:
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:

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

assume that
A76: j1 = j2 and
A77: i2 = i1 + 1 ; :: thesis:
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:

end;

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

A79: now :: thesis:

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

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

assume that
A83: j1 = j2 and
A84: i1 = i2 + 1 ; :: thesis:
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:

end;

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

A86: now :: thesis:

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

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 by A2;

suppose A92: p1 `2 = p2 `2 ; :: thesis:

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

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

end;

A97: now :: thesis:

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

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

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

end;

A103: now :: thesis:

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

end;

A105: rl `1 = rl9 `1 by EUCLID:52;

A106: now :: thesis:

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

end;

A108: now :: thesis:

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

end;

A110: now :: thesis:

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

end;

A112: now :: thesis:

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

end;

now :: thesis:

per cases by A17, A90, A92;

suppose A114: j1 = j2 + 1 ; :: thesis:

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

proof

per cases by A33, XXREAL_0:1;

suppose 1 < i2 ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A95, A114; :: thesis:

end;

suppose 1 = i2 ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A97, A114; :: thesis:

end;

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

proof

per cases by A21, XXREAL_0:1;

suppose i2 < len (GoB f) ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A112, A114; :: thesis:

end;

suppose i2 = len (GoB f) ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A106, A114; :: thesis:

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:

end;

suppose A116: j2 = j1 + 1 ; :: thesis:

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

proof

per cases by A35, XXREAL_0:1;

suppose i1 < len (GoB f) ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A110, A116; :: thesis:

end;

suppose i1 = len (GoB f) ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A108, A116; :: thesis:

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

per cases by A18, XXREAL_0:1;

suppose 1 < i1 ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A101, A116; :: thesis:

end;

suppose 1 = i1 ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A103, A116; :: thesis:

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

end;

suppose A118: p1 `1 = p2 `1 ; :: thesis:

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

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

end;

A124: now :: thesis:

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

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

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

end;

A130: now :: thesis:

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

end;

A132: rp `2 = rp9 `2 by EUCLID:52;

A133: now :: thesis:

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

end;

A135: now :: thesis:

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

end;

A137: now :: thesis:

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

end;

A139: now :: thesis:

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

end;

now :: thesis:

per cases by A17, A91, A118;

suppose A141: i1 = i2 + 1 ; :: thesis:

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

proof

per cases by A30, XXREAL_0:1;

suppose j1 < width (GoB f) ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A139, A141; :: thesis:

end;

suppose j1 = width (GoB f) ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A133, A141; :: thesis:

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

per cases by A24, XXREAL_0:1;

suppose 1 < j1 ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A137, A141; :: thesis:

end;

suppose 1 = j1 ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A122, A141; :: thesis:

end;

suppose A143: i2 = i1 + 1 ; :: thesis:

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

proof

per cases by A30, XXREAL_0:1;

suppose j1 < width (GoB f) ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A124, A143; :: thesis:

end;

suppose j1 = width (GoB f) ; :: thesis:

hence rl in Int (left_cell (f,k,(GoB f))) by A135, A143; :: thesis:

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

per cases by A24, XXREAL_0:1;

suppose 1 < j1 ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A128, A143; :: thesis:

end;

suppose 1 = j1 ; :: thesis:

hence rp in Int (right_cell (f,k,(GoB f))) by A130, A143; :: thesis:

end;

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

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

end;