let f be non empty FinSequence of (); :: 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 ;
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 () by A7, A9;
per cases ( LSeg (f,k) is horizontal or LSeg (f,k) is vertical ) by ;
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 () 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))
A13: ( j0 > j implies j0 >= j + 1 ) by NAT_1:13;
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 ;
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 ;
j >= 1 by ;
then p `2 > ((GoB f) * (1,j)) `2 by ;
hence contradiction by A7, A9, A12, A16; :: thesis: verum
end;
suppose j0 = j ; :: thesis: contradiction
then p `2 > ((GoB f) * (1,j0)) `2 by ;
hence contradiction by A7, A9, A12; :: thesis: verum
end;
suppose A17: j0 > j + 1 ; :: thesis: contradiction
then j + 1 <= width (GoB f) by ;
then j < width (GoB f) by NAT_1:13;
then A18: p `2 < ((GoB f) * (1,(j + 1))) `2 by ;
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 ;
hence contradiction by A7, A9, A12, A18; :: thesis: verum
end;
suppose A20: j0 = j + 1 ; :: thesis: contradiction
then j < width (GoB f) by ;
then p `2 < ((GoB f) * (1,j0)) `2 by ;
hence contradiction by A7, A9, A12; :: thesis: verum
end;
end;
end;
hence contradiction by A5, A4, XBOOLE_0:def 4; :: thesis: verum
end;
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 () 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))
A24: ( i0 > i implies i0 >= i + 1 ) by NAT_1:13;
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 ;
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 ;
i >= 1 by ;
then p `1 > ((GoB f) * (i,1)) `1 by ;
hence contradiction by A7, A9, A23, A27; :: thesis: verum
end;
suppose i0 = i ; :: thesis: contradiction
then p `1 > ((GoB f) * (i0,1)) `1 by ;
hence contradiction by A7, A9, A23; :: thesis: verum
end;
suppose A28: i0 > i + 1 ; :: thesis: contradiction
then i + 1 <= len (GoB f) by ;
then i < len (GoB f) by NAT_1:13;
then A29: p `1 < ((GoB f) * ((i + 1),1)) `1 by ;
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 ;
hence contradiction by A7, A9, A23, A29; :: thesis: verum
end;
suppose A31: i0 = i + 1 ; :: thesis: contradiction
then i < len (GoB f) by ;
then p `1 < ((GoB f) * (i0,1)) `1 by ;
hence contradiction by A7, A9, A23; :: thesis: verum
end;
end;
end;
hence contradiction by A5, A4, XBOOLE_0:def 4; :: thesis: verum
end;
end;