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 ;
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 ;
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 ;
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 ;
1 <= j + 1 by ;
then A17: <*((GoB f) * (1,(j + 1)))*> is_in_the_area_of f by ;
A18: L~ (SpStSeq (L~ f)) = { p where p is Point of () : ( ( 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 () 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 ;
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 ;
A28: p `1 = r by ;
A29: p `2 = s by ;
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;
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;
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;
suppose A34: p `2 = S-bound (L~ (SpStSeq (L~ f))) ; :: thesis: contradiction
A35: 1 in dom <*((GoB f) * (1,j))*> by FINSEQ_5:6;
<*((GoB f) * (1,j))*> /. 1 = (GoB f) * (1,j) by FINSEQ_4:16;
hence contradiction by A26, A15, A29, A22, A34, A35; :: thesis: verum
end;
suppose A36: p `1 = E-bound (L~ (SpStSeq (L~ f))) ; :: thesis: contradiction
A37: 1 in dom <*((GoB f) * ((i + 1),1))*> by FINSEQ_5:6;
<*((GoB f) * ((i + 1),1))*> /. 1 = (GoB f) * ((i + 1),1) by FINSEQ_4:16;
hence contradiction by A25, A10, A28, A19, A36, A37; :: thesis: verum
end;
end;