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:
assume that
A3: ( not p1 in L~ f & not p2 in L~ f ) and
A4: rng f misses LSeg p1,p2 ; :: thesis:
A5: p in {p} by TARSKI:def 1;
then A6: p in LSeg p1,p2 by A1, XBOOLE_0:def 4;
A7: p in LSeg p2,p1 by A1, A5, XBOOLE_0:def 4;
A8: f is_sequence_on GoB f by GOBOARD5:def 5;
p in L~ f by A1, A5, XBOOLE_0:def 4;
then consider LS being set such that
A9: ( p in LS & LS in { (LSeg f,i) where i is Element of NAT : ( 1 <= i & i + 1 <= len f ) } ) by TARSKI:def 4;
consider k being Element of NAT such that
A10: ( LS = LSeg f,k & 1 <= k & k + 1 <= len f ) by A9;
set G = GoB f;

A11: now

let r be Point of (TOP-REAL 2); :: thesis:
assume A12: 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:44;
hence r in right_cell f,k,(GoB f) by A12; :: thesis:
Int (right_cell f,k,(GoB f)) misses L~ f by A8, A10, JORDAN9:17;
hence not r in L~ f by A12, XBOOLE_0:3; :: thesis:

end;

A13: now

let r be Point of (TOP-REAL 2); :: thesis:
assume A14: 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:44;
hence r in left_cell f,k,(GoB f) by A14; :: thesis:
Int (left_cell f,k,(GoB f)) misses L~ f by A8, A10, JORDAN9:17;
hence not r in L~ f by A14, XBOOLE_0:3; :: thesis:

end;

consider i1, j1, i2, j2 being Element of NAT such that
A15: ( [i1,j1] in Indices (GoB f) & f /. k = (GoB f) * i1,j1 ) and
A16: ( [i2,j2] in Indices (GoB f) & 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 A8, A10, JORDAN8:6;
k < len f by A10, NAT_1:13;
then A18: k in dom f by A10, FINSEQ_3:27;
then f . k in rng f by FUNCT_1:12;
then A19: f /. k in rng f by A18, PARTFUN1:def 8;
1 <= k + 1 by A10, NAT_1:13;
then A20: k + 1 in dom f by A10, FINSEQ_3:27;
then f . (k + 1) in rng f by FUNCT_1:12;
then A21: f /. (k + 1) in rng f by A20, PARTFUN1:def 8;
A22: (LSeg p1,p2) /\ (LSeg f,k) = {p} by A1, A9, A10, TOPREAL3:26, ZFMISC_1:150;
( LSeg f,k is vertical or LSeg f,k is horizontal ) by SPPOL_1:41;
then ( LSeg (f /. k),(f /. (k + 1)) is vertical or LSeg (f /. k),(f /. (k + 1)) is horizontal ) by A10, TOPREAL1:def 5;
then A23: ( (f /. k) `1 = (f /. (k + 1)) `1 or (f /. k) `2 = (f /. (k + 1)) `2 ) by SPPOL_1:36, SPPOL_1:37;
A24: (LSeg p1,p2) /\ (LSeg (f /. k),(f /. (k + 1))) = {p} by A10, A22, TOPREAL1:def 5;
A25: ( p <> p1 & p <> p2 & p <> f /. k ) by A1, A3, A4, A5, A6, A19, XBOOLE_0:3, XBOOLE_0:def 4;
then A26: ( p1 `2 = p2 `2 implies i1 = i2 ) by A15, A16, A23, A24, Th30, JORDAN1G:7;
A27: ( p1 `1 = p2 `1 implies j1 = j2 ) by A15, A16, A23, A24, A25, Th30, JORDAN1G:6;
A28: i2 <= len (GoB f) by A16, MATRIX_1:39;
A29: 1 <= i2 by A16, MATRIX_1:39;
A30: i1 <= len (GoB f) by A15, MATRIX_1:39;
A31: 1 <= i1 by A15, MATRIX_1:39;
A32: 1 <= j1 by A15, MATRIX_1:39;
A33: j1 <= width (GoB f) by A15, MATRIX_1:39;
A34: j2 <= width (GoB f) by A16, MATRIX_1:39;
A35: 1 <= j2 by A16, MATRIX_1:39;
A36: j1 -' 1 < j1 by A32, JORDAN5B:1;
A37: i1 -' 1 < i1 by A31, JORDAN5B:1;
A38: i2 -' 1 < i2 by A29, JORDAN5B:1;
A39: p in LSeg (f /. (k + 1)),(f /. k) by A9, A10, TOPREAL1:def 5;
A40: p <> f /. (k + 1) by A4, A6, A21, XBOOLE_0:3;

A41: now

assume A42: ( i1 = i2 & j1 = j2 + 1 ) ; :: thesis:
then A43: ( 1 <= j2 + 1 & j2 + 1 <= width (GoB f) ) by A15, MATRIX_1:39;
j2 < j1 by A42, NAT_1:13;
then (f /. (k + 1)) `2 < (f /. k) `2 by A15, A16, A30, A31, A33, A35, A42, GOBOARD5:5;
then ( (f /. (k + 1)) `2 < p `2 & p `2 < (f /. k) `2 ) by A25, A39, A40, TOPREAL6:38;
hence ( ((GoB f) * 1,j2) `2 < p `2 & p `2 < ((GoB f) * 1,(j2 + 1)) `2 ) by A15, A16, A30, A31, A34, A35, A42, A43, GOBOARD5:2; :: thesis:

end;

A44: now

assume A45: ( i1 = i2 & j2 = j1 + 1 ) ; :: thesis:
then j1 < j2 by NAT_1:13;
then (f /. k) `2 < (f /. (k + 1)) `2 by A15, A16, A30, A31, A32, A34, A45, GOBOARD5:5;
then ( (f /. k) `2 < p `2 & p `2 < (f /. (k + 1)) `2 ) by A25, A39, A40, TOPREAL6:38;
hence ( ((GoB f) * 1,j1) `2 < p `2 & p `2 < ((GoB f) * 1,(j1 + 1)) `2 ) by A15, A16, A29, A30, A32, A33, A34, A35, A45, GOBOARD5:2; :: thesis:

end;

A46: now

assume A47: ( j1 = j2 & i1 = i2 + 1 ) ; :: thesis:
then i2 < i1 by NAT_1:13;
then ((GoB f) * i2,j1) `1 < ((GoB f) * i1,j1) `1 by A29, A30, A32, A33, GOBOARD5:4;
then ( (f /. (k + 1)) `1 < p `1 & p `1 < (f /. k) `1 ) by A15, A16, A25, A39, A40, A47, TOPREAL6:37;
hence ( ((GoB f) * i2,1) `1 < p `1 & p `1 < ((GoB f) * (i2 + 1),1) `1 ) by A15, A16, A28, A29, A30, A31, A34, A35, A47, GOBOARD5:3; :: thesis:

end;

A48: now

assume A49: ( j1 = j2 & i2 = i1 + 1 ) ; :: thesis:
then i1 < i2 by NAT_1:13;
then (f /. k) `1 < (f /. (k + 1)) `1 by A15, A16, A28, A31, A34, A35, A49, GOBOARD5:4;
then ( (f /. k) `1 < p `1 & p `1 < (f /. (k + 1)) `1 ) by A25, A39, A40, TOPREAL6:37;
hence ( ((GoB f) * i1,1) `1 < p `1 & p `1 < ((GoB f) * (i1 + 1),1) `1 ) by A15, A16, A28, A29, A30, A31, A33, A35, A49, GOBOARD5:3; :: thesis:

end;

A50: ( 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 A8, A10, A15, A16, GOBRD13:24, GOBRD13:25;
A51: ( i2 = i1 + 1 implies i1 < len (GoB f) ) by A28, NAT_1:13;

A52: now

assume ( 1 < j1 & i2 = i1 + 1 ) ; :: thesis:
then ( 1 <= i1 & i1 < len (GoB f) & 1 <= j1 -' 1 & j1 -' 1 < width (GoB f) ) by A15, A28, A33, A36, MATRIX_1:39, NAT_1:13, NAT_D:49, 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 GOBOARD6:29; :: thesis:

end;

A53: now

assume A54: ( 1 = j1 & i2 = i1 + 1 ) ; :: thesis:
then Int (cell (GoB f),i1,0 ) = Int (cell (GoB f),i1,(j1 -' 1)) by NAT_2:10;
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 A31, A51, A54, GOBOARD6:27; :: thesis:

end;

A55: ( 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 A31, A32, A51, GOBOARD6:29;
A56: ( 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 A31, A51, GOBOARD6:28;
A57: ( i1 = i2 + 1 implies i2 < len (GoB f) ) by A30, NAT_1:13;
A58: ( 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 A8, A10, A15, A16, GOBRD13:26, GOBRD13:27;

A59: now

assume ( 1 < j1 & i1 = i2 + 1 ) ; :: thesis:
then ( 1 <= i2 & i2 < len (GoB f) & 1 <= j1 -' 1 & j1 -' 1 < width (GoB f) ) by A16, A30, A33, A36, MATRIX_1:39, NAT_1:13, NAT_D:49, 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 GOBOARD6:29; :: thesis:

end;

A60: now

assume A61: ( 1 = j1 & i1 = i2 + 1 ) ; :: thesis:
then Int (cell (GoB f),i2,0 ) = Int (cell (GoB f),i2,(j1 -' 1)) by NAT_2:10;
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 A29, A57, A61, GOBOARD6:27; :: thesis:

end;

A62: ( 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 A29, A32, A57, GOBOARD6:29;
A63: ( 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 A29, A57, GOBOARD6:28;
A64: ( j2 = j1 + 1 implies j1 < width (GoB f) ) by A34, NAT_1:13;
A65: ( 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 A8, A10, A15, A16, GOBRD13:22, GOBRD13:23;

A66: now

assume ( 1 < i1 & j2 = j1 + 1 ) ; :: thesis:
then ( 1 <= i1 -' 1 & i1 -' 1 < len (GoB f) & 1 <= j1 & j1 < width (GoB f) ) by A15, A30, A34, A37, MATRIX_1:39, NAT_1:13, NAT_D:49, 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 GOBOARD6:29; :: thesis:

end;

A67: now

assume A68: ( 1 = i1 & j2 = j1 + 1 ) ; :: thesis:
then Int (cell (GoB f),(i1 -' 1),j1) = Int (cell (GoB f),0 ,j1) by NAT_2:10;
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 A32, A64, A68, GOBOARD6:23; :: thesis:

end;

A69: ( 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 A31, A32, A64, GOBOARD6:29;
A70: ( 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 A32, A64, GOBOARD6:26;
A71: ( j1 = j2 + 1 implies j2 < width (GoB f) ) by A33, NAT_1:13;
A72: ( 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 A8, A10, A15, A16, GOBRD13:28, GOBRD13:29;

A73: now

assume ( 1 < i2 & j1 = j2 + 1 ) ; :: thesis:
then ( 1 <= i2 -' 1 & i2 -' 1 < len (GoB f) & 1 <= j2 & j2 < width (GoB f) ) by A16, A28, A33, A38, MATRIX_1:39, NAT_1:13, NAT_D:49, 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 GOBOARD6:29; :: thesis:

end;

A74: now

assume A75: ( 1 = i2 & j1 = j2 + 1 ) ; :: thesis:
then Int (cell (GoB f),(i2 -' 1),j2) = Int (cell (GoB f),0 ,j2) by NAT_2:10;
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 A35, A71, A75, GOBOARD6:23; :: thesis:

end;

A76: ( 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, A35, A71, GOBOARD6:29;
A77: ( 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 A35, A71, GOBOARD6:26;

per cases by A2;

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

then A79: p `2 = p1 `2 by A7, GOBOARD7:6;
Int (left_cell f,k,(GoB f)) <> {} by A8, A10, JORDAN9:11;
then consider rl' being set such that
A80: rl' in Int (left_cell f,k,(GoB f)) by XBOOLE_0:def 1;
reconsider rl' = rl' as Point of (TOP-REAL 2) by A80;
reconsider rl = |[(rl' `1 ),(p `2 )]| as Point of (TOP-REAL 2) ;
A81: ( rl `2 = p `2 & rl `1 = rl' `1 ) by EUCLID:56;
Int (right_cell f,k,(GoB f)) <> {} by A8, A10, JORDAN9:11;
then consider rp' being set such that
A82: rp' in Int (right_cell f,k,(GoB f)) by XBOOLE_0:def 1;
reconsider rp' = rp' as Point of (TOP-REAL 2) by A82;
reconsider rp = |[(rp' `1 ),(p `2 )]| as Point of (TOP-REAL 2) ;
A83: ( rp `2 = p `2 & rp `1 = rp' `1 ) by EUCLID:56;

A84: now

assume A85: ( j1 = j2 + 1 & i2 < len (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rl' = |[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 A15, A16, A23, A24, A25, A72, A76, A78, A80, Th30, JORDAN1G:7;
then ( ((GoB f) * i2,1) `1 < rl `1 & rl `1 < ((GoB f) * (i2 + 1),1) `1 & ((GoB f) * 1,j2) `2 < p `2 & p `2 < ((GoB f) * 1,(j2 + 1)) `2 ) by A15, A16, A23, A24, A25, A41, A78, A81, A85, Th30, EUCLID:56, JORDAN1G:7;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A72, A76, A78, A81, A85, Th30, JORDAN1G:7; :: thesis:

end;

A86: now

assume A87: ( j1 = j2 + 1 & i2 = len (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rl' = |[r,s]| & ((GoB f) * (len (GoB f)),1) `1 < r & ((GoB f) * 1,j2) `2 < s & s < ((GoB f) * 1,(j2 + 1)) `2 ) by A15, A16, A23, A24, A25, A72, A77, A78, A80, Th30, JORDAN1G:7;
then ( ((GoB f) * (len (GoB f)),1) `1 < rl `1 & ((GoB f) * 1,j2) `2 < p `2 & p `2 < ((GoB f) * 1,(j2 + 1)) `2 ) by A15, A16, A23, A24, A25, A41, A78, A81, A87, Th30, EUCLID:56, JORDAN1G:7;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A72, A77, A78, A81, A87, Th30, JORDAN1G:7; :: thesis:

end;

A88: now

assume A89: ( j1 = j2 + 1 & 1 = i2 ) ; :: thesis:
then ex r, s being Real st
( rp' = |[r,s]| & r < ((GoB f) * 1,1) `1 & ((GoB f) * 1,j2) `2 < s & s < ((GoB f) * 1,(j2 + 1)) `2 ) by A15, A16, A23, A24, A25, A72, A74, A78, A82, Th30, JORDAN1G:7;
then rp' `1 < ((GoB f) * 1,1) `1 by EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A41, A72, A74, A78, A89, Th30, JORDAN1G:7; :: thesis:

end;

A90: now

assume A91: ( j1 = j2 + 1 & 1 < i2 ) ; :: thesis:
then ex r, s being Real st
( rp' = |[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 A15, A16, A23, A24, A25, A72, A73, A78, A82, Th30, JORDAN1G:7;
then ( ((GoB f) * (i2 -' 1),1) `1 < rp' `1 & rp' `1 < ((GoB f) * ((i2 -' 1) + 1),1) `1 ) by EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A41, A72, A73, A78, A91, Th30, JORDAN1G:7; :: thesis:

end;

A92: now

assume A93: ( j2 = j1 + 1 & i1 < len (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rp' = |[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 A15, A16, A23, A24, A25, A65, A69, A78, A82, Th30, JORDAN1G:7;
then ( ((GoB f) * i1,1) `1 < rp' `1 & rp' `1 < ((GoB f) * (i1 + 1),1) `1 ) by EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A44, A65, A69, A78, A93, Th30, JORDAN1G:7; :: thesis:

end;

A94: now

assume A95: ( j2 = j1 + 1 & i1 = len (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rp' = |[r,s]| & ((GoB f) * (len (GoB f)),1) `1 < r & ((GoB f) * 1,j1) `2 < s & s < ((GoB f) * 1,(j1 + 1)) `2 ) by A15, A16, A23, A24, A25, A65, A70, A78, A82, Th30, JORDAN1G:7;
then ((GoB f) * (len (GoB f)),1) `1 < rp' `1 by EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A44, A65, A70, A78, A95, Th30, JORDAN1G:7; :: thesis:

end;

A96: now

assume A97: ( j2 = j1 + 1 & 1 = i1 ) ; :: thesis:
then ex r, s being Real st
( rl' = |[r,s]| & r < ((GoB f) * 1,1) `1 & ((GoB f) * 1,j1) `2 < s & s < ((GoB f) * 1,(j1 + 1)) `2 ) by A15, A16, A23, A24, A25, A65, A67, A78, A80, Th30, JORDAN1G:7;
then rl' `1 < ((GoB f) * 1,1) `1 by EUCLID:56;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A44, A65, A67, A78, A97, Th30, JORDAN1G:7; :: thesis:

end;

A98: now

assume A99: ( j2 = j1 + 1 & 1 < i1 ) ; :: thesis:
then ex r, s being Real st
( rl' = |[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 A15, A16, A23, A24, A25, A65, A66, A78, A80, Th30, JORDAN1G:7;
then ( ((GoB f) * (i1 -' 1),1) `1 < rl' `1 & rl' `1 < ((GoB f) * ((i1 -' 1) + 1),1) `1 ) by EUCLID:56;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A44, A65, A66, A78, A99, Th30, JORDAN1G:7; :: thesis:

end;

now

per cases by A17, A26, A78;

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

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

proof

per cases by A28, XXREAL_0:1;

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

hence rl in Int (left_cell f,k,(GoB f)) by A84, A100; :: thesis:

end;

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

hence rl in Int (left_cell f,k,(GoB f)) by A86, A100; :: thesis:

end;

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

proof

per cases by A29, XXREAL_0:1;

suppose 1 < i2 ; :: thesis:

hence rp in Int (right_cell f,k,(GoB f)) by A90, A100; :: thesis:

end;

suppose 1 = i2 ; :: thesis:

hence rp in Int (right_cell f,k,(GoB f)) by A88, A100; :: thesis:

end;

A103: rl in left_cell f,k,(GoB f) by A13, A101;
A104: rp in right_cell f,k,(GoB f) by A11, A102;
A105: not rl in L~ f by A13, A101;
not rp in L~ f by A11, A102;
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, A3, A9, A10, A78, A79, A81, A83, A103, A104, A105, Th32; :: thesis:

end;

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

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

proof

per cases by A31, XXREAL_0:1;

suppose 1 < i1 ; :: thesis:

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

end;

suppose 1 = i1 ; :: thesis:

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

end;

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

proof

per cases by A30, XXREAL_0:1;

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

hence rp in Int (right_cell f,k,(GoB f)) by A92, A106; :: thesis:

end;

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

hence rp in Int (right_cell f,k,(GoB f)) by A94, A106; :: thesis:

end;

A109: rl in left_cell f,k,(GoB f) by A13, A107;
A110: rp in right_cell f,k,(GoB f) by A11, A108;
A111: not rl in L~ f by A13, A107;
not rp in L~ f by A11, A108;
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, A3, A9, A10, A78, A79, A81, A83, A109, A110, A111, Th32; :: 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 A112: p1 `1 = p2 `1 ; :: thesis:

then A113: p `1 = p1 `1 by A7, GOBOARD7:5;
Int (left_cell f,k,(GoB f)) <> {} by A8, A10, JORDAN9:11;
then consider rl' being set such that
A114: rl' in Int (left_cell f,k,(GoB f)) by XBOOLE_0:def 1;
reconsider rl' = rl' as Point of (TOP-REAL 2) by A114;
reconsider rl = |[(p `1 ),(rl' `2 )]| as Point of (TOP-REAL 2) ;
A115: ( rl `1 = p `1 & rl `2 = rl' `2 ) by EUCLID:56;
Int (right_cell f,k,(GoB f)) <> {} by A8, A10, JORDAN9:11;
then consider rp' being set such that
A116: rp' in Int (right_cell f,k,(GoB f)) by XBOOLE_0:def 1;
reconsider rp' = rp' as Point of (TOP-REAL 2) by A116;
reconsider rp = |[(p `1 ),(rp' `2 )]| as Point of (TOP-REAL 2) ;
A117: ( rp `1 = p `1 & rp `2 = rp' `2 ) by EUCLID:56;

A118: now

assume A119: ( i1 = i2 + 1 & j1 < width (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rp' = |[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 A15, A16, A23, A24, A25, A58, A62, A112, A116, Th30, JORDAN1G:6;
then ( ((GoB f) * 1,j1) `2 < rp `2 & rp `2 < ((GoB f) * 1,(j1 + 1)) `2 ) by A117, EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A46, A58, A62, A112, A117, A119, Th30, JORDAN1G:6; :: thesis:

end;

A120: now

assume A121: ( i1 = i2 + 1 & j1 = width (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rp' = |[r,s]| & ((GoB f) * i2,1) `1 < r & r < ((GoB f) * (i2 + 1),1) `1 & ((GoB f) * 1,(width (GoB f))) `2 < s ) by A15, A16, A23, A24, A25, A58, A63, A112, A116, Th30, JORDAN1G:6;
then ( ((GoB f) * i2,1) `1 < p `1 & p `1 < ((GoB f) * (i2 + 1),1) `1 & ((GoB f) * 1,(width (GoB f))) `2 < rp `2 ) by A15, A16, A23, A24, A25, A46, A112, A117, A121, Th30, EUCLID:56, JORDAN1G:6;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A58, A63, A112, A117, A121, Th30, JORDAN1G:6; :: thesis:

end;

A122: now

assume A123: ( i1 = i2 + 1 & 1 = j1 ) ; :: thesis:
then ex r, s being Real st
( rl' = |[r,s]| & ((GoB f) * i2,1) `1 < r & r < ((GoB f) * (i2 + 1),1) `1 & s < ((GoB f) * 1,1) `2 ) by A15, A16, A23, A24, A25, A58, A60, A112, A114, Th30, JORDAN1G:6;
then rl `2 < ((GoB f) * 1,1) `2 by A115, EUCLID:56;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A46, A58, A60, A112, A115, A123, Th30, JORDAN1G:6; :: thesis:

end;

A124: now

assume A125: ( i1 = i2 + 1 & 1 < j1 ) ; :: thesis:
then ex r, s being Real st
( rl' = |[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 A15, A16, A23, A24, A25, A58, A59, A112, A114, Th30, JORDAN1G:6;
then ( ((GoB f) * 1,(j1 -' 1)) `2 < rl' `2 & rl' `2 < ((GoB f) * 1,((j1 -' 1) + 1)) `2 ) by EUCLID:56;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A46, A58, A59, A112, A125, Th30, JORDAN1G:6; :: thesis:

end;

A126: now

assume A127: ( i2 = i1 + 1 & j1 < width (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rl' = |[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 A15, A16, A23, A24, A25, A50, A55, A112, A114, Th30, JORDAN1G:6;
then ( ((GoB f) * 1,j1) `2 < rl `2 & rl `2 < ((GoB f) * 1,(j1 + 1)) `2 ) by A115, EUCLID:56;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A48, A50, A55, A112, A115, A127, Th30, JORDAN1G:6; :: thesis:

end;

A128: now

assume A129: ( i2 = i1 + 1 & j1 = width (GoB f) ) ; :: thesis:
then ex r, s being Real st
( rl' = |[r,s]| & ((GoB f) * i1,1) `1 < r & r < ((GoB f) * (i1 + 1),1) `1 & ((GoB f) * 1,(width (GoB f))) `2 < s ) by A15, A16, A23, A24, A25, A50, A56, A112, A114, Th30, JORDAN1G:6;
then ((GoB f) * 1,(width (GoB f))) `2 < rl' `2 by EUCLID:56;
hence rl in Int (left_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A48, A50, A56, A112, A129, Th30, JORDAN1G:6; :: thesis:

end;

A130: now

assume A131: ( i2 = i1 + 1 & 1 = j1 ) ; :: thesis:
then ex r, s being Real st
( rp' = |[r,s]| & ((GoB f) * i1,1) `1 < r & r < ((GoB f) * (i1 + 1),1) `1 & s < ((GoB f) * 1,1) `2 ) by A15, A16, A23, A24, A25, A50, A53, A112, A116, Th30, JORDAN1G:6;
then rp' `2 < ((GoB f) * 1,1) `2 by EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A48, A50, A53, A112, A131, Th30, JORDAN1G:6; :: thesis:

end;

A132: now

assume A133: ( i2 = i1 + 1 & 1 < j1 ) ; :: thesis:
then ex r, s being Real st
( rp' = |[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 A15, A16, A23, A24, A25, A50, A52, A112, A116, Th30, JORDAN1G:6;
then ( ((GoB f) * 1,(j1 -' 1)) `2 < rp' `2 & rp' `2 < ((GoB f) * 1,((j1 -' 1) + 1)) `2 ) by EUCLID:56;
hence rp in Int (right_cell f,k,(GoB f)) by A15, A16, A23, A24, A25, A48, A50, A52, A112, A133, Th30, JORDAN1G:6; :: thesis:

end;

now

per cases by A17, A27, A112;

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

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

proof

per cases by A32, XXREAL_0:1;

suppose 1 < j1 ; :: thesis:

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

end;

suppose 1 = j1 ; :: thesis:

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

end;

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

proof

per cases by A33, XXREAL_0:1;

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

hence rp in Int (right_cell f,k,(GoB f)) by A118, A134; :: thesis:

end;

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

hence rp in Int (right_cell f,k,(GoB f)) by A120, A134; :: thesis:

end;

A137: rl in left_cell f,k,(GoB f) by A13, A135;
A138: rp in right_cell f,k,(GoB f) by A11, A136;
A139: not rl in L~ f by A13, A135;
not rp in L~ f by A11, A136;
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, A3, A9, A10, A112, A113, A115, A117, A137, A138, A139, Th32; :: thesis:

end;

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

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

proof

per cases by A32, XXREAL_0:1;

suppose 1 < j1 ; :: thesis:

hence rp in Int (right_cell f,k,(GoB f)) by A132, A140; :: thesis:

end;

suppose 1 = j1 ; :: thesis:

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

end;

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

proof

per cases by A33, XXREAL_0:1;

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

hence rl in Int (left_cell f,k,(GoB f)) by A126, A140; :: thesis:

end;

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

hence rl in Int (left_cell f,k,(GoB f)) by A128, A140; :: thesis:

end;

then A143: rl in left_cell f,k,(GoB f) by A13;
A144: rp in right_cell f,k,(GoB f) by A11, A141;
A145: not rl in L~ f by A13, A142;
not rp in L~ f by A11, A141;
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, A3, A9, A10, A112, A113, A115, A117, A143, A144, A145, Th32; :: 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;