let i, j be Nat; 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; ( 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)
; 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))
; 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;