let f be non empty FinSequence of (TOP-REAL 2); :: thesis: for i, j being Nat st f is special & i <= len (GoB f) & j <= width (GoB f) holds

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

let i, j be Nat; :: thesis: ( f is special & i <= len (GoB f) & j <= width (GoB f) implies Int (cell ((GoB f),i,j)) misses L~ f )

assume that

A1: f is special and

A2: i <= len (GoB f) and

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

A4: Int (cell ((GoB f),i,j)) = Int ((v_strip ((GoB f),i)) /\ (h_strip ((GoB f),j))) by GOBOARD5:def 3

.= (Int (v_strip ((GoB f),i))) /\ (Int (h_strip ((GoB f),j))) by TOPS_1:17 ;

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

then consider x being object such that

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

A6: x in L~ f by XBOOLE_0:3;

L~ f = union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by TOPREAL1:def 4;

then consider X being set such that

A7: x in X and

A8: X in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A6, TARSKI:def 4;

consider k being Nat such that

A9: X = LSeg (f,k) and

1 <= k and

k + 1 <= len f by A8;

reconsider p = x as Point of (TOP-REAL 2) by A7, A9;

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

let i, j be Nat; :: thesis: ( f is special & i <= len (GoB f) & j <= width (GoB f) implies Int (cell ((GoB f),i,j)) misses L~ f )

assume that

A1: f is special and

A2: i <= len (GoB f) and

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

A4: Int (cell ((GoB f),i,j)) = Int ((v_strip ((GoB f),i)) /\ (h_strip ((GoB f),j))) by GOBOARD5:def 3

.= (Int (v_strip ((GoB f),i))) /\ (Int (h_strip ((GoB f),j))) by TOPS_1:17 ;

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

then consider x being object such that

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

A6: x in L~ f by XBOOLE_0:3;

L~ f = union { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by TOPREAL1:def 4;

then consider X being set such that

A7: x in X and

A8: X in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A6, TARSKI:def 4;

consider k being Nat such that

A9: X = LSeg (f,k) and

1 <= k and

k + 1 <= len f by A8;

reconsider p = x as Point of (TOP-REAL 2) by A7, A9;

per cases
( LSeg (f,k) is horizontal or LSeg (f,k) is vertical )
by A1, SPPOL_1:19;

end;

suppose
LSeg (f,k) is horizontal
; :: thesis: contradiction

then consider j0 being Nat such that

A10: 1 <= j0 and

A11: j0 <= width (GoB f) and

A12: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `2 = ((GoB f) * (1,j0)) `2 by Th10;

end;A10: 1 <= j0 and

A11: j0 <= width (GoB f) and

A12: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `2 = ((GoB f) * (1,j0)) `2 by Th10;

now :: thesis: not p in Int (h_strip ((GoB f),j))

hence
contradiction
by A5, A4, XBOOLE_0:def 4; :: thesis: verumA13:
( j0 > j implies j0 >= j + 1 )
by NAT_1:13;

assume A14: p in Int (h_strip ((GoB f),j)) ; :: thesis: contradiction

end;assume A14: p in Int (h_strip ((GoB f),j)) ; :: thesis: contradiction

per cases
( j0 < j or j0 = j or j0 > j + 1 or j0 = j + 1 )
by A13, XXREAL_0:1;

end;

suppose A15:
j0 < j
; :: thesis: contradiction

0 <> len (GoB f)
by MATRIX_0:def 10;

then 1 <= len (GoB f) by NAT_1:14;

then A16: ((GoB f) * (1,j)) `2 > ((GoB f) * (1,j0)) `2 by A3, A10, A15, GOBOARD5:4;

j >= 1 by A10, A15, XXREAL_0:2;

then p `2 > ((GoB f) * (1,j)) `2 by A3, A14, GOBOARD6:27;

hence contradiction by A7, A9, A12, A16; :: thesis: verum

end;then 1 <= len (GoB f) by NAT_1:14;

then A16: ((GoB f) * (1,j)) `2 > ((GoB f) * (1,j0)) `2 by A3, A10, A15, GOBOARD5:4;

j >= 1 by A10, A15, XXREAL_0:2;

then p `2 > ((GoB f) * (1,j)) `2 by A3, A14, GOBOARD6:27;

hence contradiction by A7, A9, A12, A16; :: thesis: verum

suppose
j0 = j
; :: thesis: contradiction

then
p `2 > ((GoB f) * (1,j0)) `2
by A10, A11, A14, GOBOARD6:27;

hence contradiction by A7, A9, A12; :: thesis: verum

end;hence contradiction by A7, A9, A12; :: thesis: verum

suppose A17:
j0 > j + 1
; :: thesis: contradiction

then
j + 1 <= width (GoB f)
by A11, XXREAL_0:2;

then j < width (GoB f) by NAT_1:13;

then A18: p `2 < ((GoB f) * (1,(j + 1))) `2 by A14, GOBOARD6:28;

0 <> len (GoB f) by MATRIX_0:def 10;

then A19: 1 <= len (GoB f) by NAT_1:14;

j + 1 >= 1 by NAT_1:11;

then ((GoB f) * (1,(j + 1))) `2 < ((GoB f) * (1,j0)) `2 by A11, A17, A19, GOBOARD5:4;

hence contradiction by A7, A9, A12, A18; :: thesis: verum

end;then j < width (GoB f) by NAT_1:13;

then A18: p `2 < ((GoB f) * (1,(j + 1))) `2 by A14, GOBOARD6:28;

0 <> len (GoB f) by MATRIX_0:def 10;

then A19: 1 <= len (GoB f) by NAT_1:14;

j + 1 >= 1 by NAT_1:11;

then ((GoB f) * (1,(j + 1))) `2 < ((GoB f) * (1,j0)) `2 by A11, A17, A19, GOBOARD5:4;

hence contradiction by A7, A9, A12, A18; :: thesis: verum

suppose
LSeg (f,k) is vertical
; :: thesis: contradiction

then consider i0 being Nat such that

A21: 1 <= i0 and

A22: i0 <= len (GoB f) and

A23: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i0,1)) `1 by Th11;

end;A21: 1 <= i0 and

A22: i0 <= len (GoB f) and

A23: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds

p `1 = ((GoB f) * (i0,1)) `1 by Th11;

now :: thesis: not p in Int (v_strip ((GoB f),i))

hence
contradiction
by A5, A4, XBOOLE_0:def 4; :: thesis: verumA24:
( i0 > i implies i0 >= i + 1 )
by NAT_1:13;

assume A25: p in Int (v_strip ((GoB f),i)) ; :: thesis: contradiction

end;assume A25: p in Int (v_strip ((GoB f),i)) ; :: thesis: contradiction

per cases
( i0 < i or i0 = i or i0 > i + 1 or i0 = i + 1 )
by A24, XXREAL_0:1;

end;

suppose A26:
i0 < i
; :: thesis: contradiction

0 <> width (GoB f)
by MATRIX_0:def 10;

then 1 <= width (GoB f) by NAT_1:14;

then A27: ((GoB f) * (i,1)) `1 > ((GoB f) * (i0,1)) `1 by A2, A21, A26, GOBOARD5:3;

i >= 1 by A21, A26, XXREAL_0:2;

then p `1 > ((GoB f) * (i,1)) `1 by A2, A25, GOBOARD6:29;

hence contradiction by A7, A9, A23, A27; :: thesis: verum

end;then 1 <= width (GoB f) by NAT_1:14;

then A27: ((GoB f) * (i,1)) `1 > ((GoB f) * (i0,1)) `1 by A2, A21, A26, GOBOARD5:3;

i >= 1 by A21, A26, XXREAL_0:2;

then p `1 > ((GoB f) * (i,1)) `1 by A2, A25, GOBOARD6:29;

hence contradiction by A7, A9, A23, A27; :: thesis: verum

suppose
i0 = i
; :: thesis: contradiction

then
p `1 > ((GoB f) * (i0,1)) `1
by A21, A22, A25, GOBOARD6:29;

hence contradiction by A7, A9, A23; :: thesis: verum

end;hence contradiction by A7, A9, A23; :: thesis: verum

suppose A28:
i0 > i + 1
; :: thesis: contradiction

then
i + 1 <= len (GoB f)
by A22, XXREAL_0:2;

then i < len (GoB f) by NAT_1:13;

then A29: p `1 < ((GoB f) * ((i + 1),1)) `1 by A25, GOBOARD6:30;

0 <> width (GoB f) by MATRIX_0:def 10;

then A30: 1 <= width (GoB f) by NAT_1:14;

i + 1 >= 1 by NAT_1:11;

then ((GoB f) * ((i + 1),1)) `1 < ((GoB f) * (i0,1)) `1 by A22, A28, A30, GOBOARD5:3;

hence contradiction by A7, A9, A23, A29; :: thesis: verum

end;then i < len (GoB f) by NAT_1:13;

then A29: p `1 < ((GoB f) * ((i + 1),1)) `1 by A25, GOBOARD6:30;

0 <> width (GoB f) by MATRIX_0:def 10;

then A30: 1 <= width (GoB f) by NAT_1:14;

i + 1 >= 1 by NAT_1:11;

then ((GoB f) * ((i + 1),1)) `1 < ((GoB f) * (i0,1)) `1 by A22, A28, A30, GOBOARD5:3;

hence contradiction by A7, A9, A23, A29; :: thesis: verum