let i, j be Nat; :: thesis: for f being V22() standard special_circular_sequence st 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) holds

Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))

let f be V22() standard special_circular_sequence; :: thesis: ( 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) implies Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) )

assume that

A1: 1 <= i and

A2: i < len (GoB f) and

A3: 1 <= j and

A4: j < width (GoB f) ; :: thesis: Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))

A5: i + 1 <= len (GoB f) by A2, NAT_1:13;

set G = GoB f;

A6: Int (cell ((GoB f),i,j)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i,1)) `1 < r & r < ((GoB f) * ((i + 1),1)) `1 & ((GoB f) * (1,j)) `2 < s & s < ((GoB f) * (1,(j + 1))) `2 ) } by A1, A2, A3, A4, GOBOARD6:26;

A7: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;

A8: 1 <= width (GoB f) by GOBRD11:34;

then A9: <*((GoB f) * (i,1))*> is_in_the_area_of f by A1, A2, Th49;

1 <= i + 1 by A1, NAT_1:13;

then A10: <*((GoB f) * ((i + 1),1))*> is_in_the_area_of f by A8, A5, Th49;

assume Int (cell ((GoB f),i,j)) meets L~ (SpStSeq (L~ f)) ; :: thesis: contradiction

then consider x being object such that

A11: x in Int (cell ((GoB f),i,j)) and

A12: x in L~ (SpStSeq (L~ f)) by XBOOLE_0:3;

A13: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;

A14: 1 <= len (GoB f) by GOBRD11:34;

then A15: <*((GoB f) * (1,j))*> is_in_the_area_of f by A3, A4, Th49;

A16: j + 1 <= width (GoB f) by A4, NAT_1:13;

1 <= j + 1 by A3, NAT_1:13;

then A17: <*((GoB f) * (1,(j + 1)))*> is_in_the_area_of f by A14, A16, Th49;

A18: L~ (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) } by Th35;

A19: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;

consider p being Point of (TOP-REAL 2) such that

A20: p = x and

A21: ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) by A12, A18;

A22: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;

consider r, s being Real such that

A23: x = |[r,s]| and

A24: ((GoB f) * (i,1)) `1 < r and

A25: r < ((GoB f) * ((i + 1),1)) `1 and

A26: ((GoB f) * (1,j)) `2 < s and

A27: s < ((GoB f) * (1,(j + 1))) `2 by A6, A11;

A28: p `1 = r by A23, A20, EUCLID:52;

A29: p `2 = s by A23, A20, EUCLID:52;

Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))

let f be V22() standard special_circular_sequence; :: thesis: ( 1 <= i & i < len (GoB f) & 1 <= j & j < width (GoB f) implies Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f)) )

assume that

A1: 1 <= i and

A2: i < len (GoB f) and

A3: 1 <= j and

A4: j < width (GoB f) ; :: thesis: Int (cell ((GoB f),i,j)) misses L~ (SpStSeq (L~ f))

A5: i + 1 <= len (GoB f) by A2, NAT_1:13;

set G = GoB f;

A6: Int (cell ((GoB f),i,j)) = { |[r,s]| where r, s is Real : ( ((GoB f) * (i,1)) `1 < r & r < ((GoB f) * ((i + 1),1)) `1 & ((GoB f) * (1,j)) `2 < s & s < ((GoB f) * (1,(j + 1))) `2 ) } by A1, A2, A3, A4, GOBOARD6:26;

A7: N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) by SPRECT_1:60;

A8: 1 <= width (GoB f) by GOBRD11:34;

then A9: <*((GoB f) * (i,1))*> is_in_the_area_of f by A1, A2, Th49;

1 <= i + 1 by A1, NAT_1:13;

then A10: <*((GoB f) * ((i + 1),1))*> is_in_the_area_of f by A8, A5, Th49;

assume Int (cell ((GoB f),i,j)) meets L~ (SpStSeq (L~ f)) ; :: thesis: contradiction

then consider x being object such that

A11: x in Int (cell ((GoB f),i,j)) and

A12: x in L~ (SpStSeq (L~ f)) by XBOOLE_0:3;

A13: W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) by SPRECT_1:58;

A14: 1 <= len (GoB f) by GOBRD11:34;

then A15: <*((GoB f) * (1,j))*> is_in_the_area_of f by A3, A4, Th49;

A16: j + 1 <= width (GoB f) by A4, NAT_1:13;

1 <= j + 1 by A3, NAT_1:13;

then A17: <*((GoB f) * (1,(j + 1)))*> is_in_the_area_of f by A14, A16, Th49;

A18: L~ (SpStSeq (L~ f)) = { p where p is Point of (TOP-REAL 2) : ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) } by Th35;

A19: E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) by SPRECT_1:61;

consider p being Point of (TOP-REAL 2) such that

A20: p = x and

A21: ( ( p `1 = W-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = N-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 <= E-bound (L~ (SpStSeq (L~ f))) & p `1 >= W-bound (L~ (SpStSeq (L~ f))) & p `2 = S-bound (L~ (SpStSeq (L~ f))) ) or ( p `1 = E-bound (L~ (SpStSeq (L~ f))) & p `2 <= N-bound (L~ (SpStSeq (L~ f))) & p `2 >= S-bound (L~ (SpStSeq (L~ f))) ) ) by A12, A18;

A22: S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) by SPRECT_1:59;

consider r, s being Real such that

A23: x = |[r,s]| and

A24: ((GoB f) * (i,1)) `1 < r and

A25: r < ((GoB f) * ((i + 1),1)) `1 and

A26: ((GoB f) * (1,j)) `2 < s and

A27: s < ((GoB f) * (1,(j + 1))) `2 by A6, A11;

A28: p `1 = r by A23, A20, EUCLID:52;

A29: p `2 = s by A23, A20, EUCLID:52;

per cases
( p `1 = W-bound (L~ (SpStSeq (L~ f))) or p `2 = N-bound (L~ (SpStSeq (L~ f))) or p `2 = S-bound (L~ (SpStSeq (L~ f))) or p `1 = E-bound (L~ (SpStSeq (L~ f))) )
by A21;

end;

suppose A30:
p `1 = W-bound (L~ (SpStSeq (L~ f)))
; :: thesis: contradiction

A31:
1 in dom <*((GoB f) * (i,1))*>
by FINSEQ_5:6;

<*((GoB f) * (i,1))*> /. 1 = (GoB f) * (i,1) by FINSEQ_4:16;

hence contradiction by A24, A9, A28, A13, A30, A31; :: thesis: verum

end;<*((GoB f) * (i,1))*> /. 1 = (GoB f) * (i,1) by FINSEQ_4:16;

hence contradiction by A24, A9, A28, A13, A30, A31; :: thesis: verum

suppose A32:
p `2 = N-bound (L~ (SpStSeq (L~ f)))
; :: thesis: contradiction

A33:
1 in dom <*((GoB f) * (1,(j + 1)))*>
by FINSEQ_5:6;

<*((GoB f) * (1,(j + 1)))*> /. 1 = (GoB f) * (1,(j + 1)) by FINSEQ_4:16;

hence contradiction by A27, A17, A29, A7, A32, A33; :: thesis: verum

end;<*((GoB f) * (1,(j + 1)))*> /. 1 = (GoB f) * (1,(j + 1)) by FINSEQ_4:16;

hence contradiction by A27, A17, A29, A7, A32, A33; :: thesis: verum