let i, j be Element of NAT ; :: thesis: for f being non constant 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 non constant 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 & i < len (GoB f) )
and
A2:
( 1 <= j & j < width (GoB f) )
; :: thesis: Int (cell (GoB f),i,j) misses L~ (SpStSeq (L~ f))
set G = GoB f;
A3:
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, GOBOARD6:29;
assume
Int (cell (GoB f),i,j) meets L~ (SpStSeq (L~ f))
; :: thesis: contradiction
then consider x being set such that
A4:
x in Int (cell (GoB f),i,j)
and
A5:
x in L~ (SpStSeq (L~ f))
by XBOOLE_0:3;
consider r, s being Real such that
A6:
x = |[r,s]|
and
A7:
( ((GoB f) * i,1) `1 < r & r < ((GoB f) * (i + 1),1) `1 )
and
A8:
( ((GoB f) * 1,j) `2 < s & s < ((GoB f) * 1,(j + 1)) `2 )
by A3, A4;
A9:
1 <= width (GoB f)
by GOBRD11:34;
then A10:
<*((GoB f) * i,1)*> is_in_the_area_of f
by A1, Th66;
A11:
1 <= len (GoB f)
by GOBRD11:34;
then A12:
<*((GoB f) * 1,j)*> is_in_the_area_of f
by A2, Th66;
( 1 <= i + 1 & i + 1 <= len (GoB f) )
by A1, NAT_1:13;
then A13:
<*((GoB f) * (i + 1),1)*> is_in_the_area_of f
by A9, Th66;
( 1 <= j + 1 & j + 1 <= width (GoB f) )
by A2, NAT_1:13;
then A14:
<*((GoB f) * 1,(j + 1))*> is_in_the_area_of f
by A11, Th66;
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 Th52;
then consider p being Point of (TOP-REAL 2) such that
A15:
p = x
and
A16:
( ( 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 A5;
A17:
p `1 = r
by A6, A15, EUCLID:56;
A18:
p `2 = s
by A6, A15, EUCLID:56;
A19:
( W-bound (L~ (SpStSeq (L~ f))) = W-bound (L~ f) & S-bound (L~ (SpStSeq (L~ f))) = S-bound (L~ f) & N-bound (L~ (SpStSeq (L~ f))) = N-bound (L~ f) & E-bound (L~ (SpStSeq (L~ f))) = E-bound (L~ f) )
by SPRECT_1:66, SPRECT_1:67, SPRECT_1:68, SPRECT_1:69;