let G be Go-board; :: thesis: for f being FinSequence of (TOP-REAL 2) st f is_sequence_on G & f is special holds
for i, j being Nat st i <= len G & j <= width G holds
Int (cell (G,i,j)) misses L~ f
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & f is special implies for i, j being Nat st i <= len G & j <= width G holds
Int (cell (G,i,j)) misses L~ f )
assume that
A1: f is_sequence_on G and
A2: f is special ; :: thesis: for i, j being Nat st i <= len G & j <= width G holds
Int (cell (G,i,j)) misses L~ f
let i, j be Nat; :: thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) misses L~ f )
assume that
A3: i <= len G and
A4: j <= width G ; :: thesis: Int (cell (G,i,j)) misses L~ f
A5: Int (cell (G,i,j)) = (Int (v_strip (G,i))) /\ (Int (h_strip (G,j))) by TOPS_1:17;
assume Int (cell (G,i,j)) meets L~ f ; :: thesis: contradiction
then consider x being object such that
A6: x in Int (cell (G,i,j)) and
A7: 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
A8: x in X and
A9: X in { (LSeg (f,k)) where k is Nat : ( 1 <= k & k + 1 <= len f ) } by A7, TARSKI:def 4;
consider k being Nat such that
A10: X = LSeg (f,k) and
1 <= k and
k + 1 <= len f by A9;
reconsider p = x as Point of (TOP-REAL 2) by A8, A10;

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

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

then consider j0 being Nat such that
A11: 1 <= j0 and
A12: j0 <= width G and
A13: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `2 = (G * (1,j0)) `2 by A1, Th12;

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

A14: ( j0 > j implies j0 >= j + 1 ) by NAT_1:13;
assume A15: p in Int (h_strip (G,j)) ; :: thesis: contradiction

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

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

0 <> len G by MATRIX_0:def 10;
then 1 <= len G by NAT_1:14;
then A17: (G * (1,j)) `2 > (G * (1,j0)) `2 by A4, A11, A16, GOBOARD5:4;
j >= 1 by A11, A16, XXREAL_0:2;
then p `2 > (G * (1,j)) `2 by A4, A15, GOBOARD6:27;
hence contradiction by A8, A10, A13, A17; :: thesis: verum

end;

suppose j0 = j ; :: thesis: contradiction

then p `2 > (G * (1,j0)) `2 by A11, A12, A15, GOBOARD6:27;
hence contradiction by A8, A10, A13; :: thesis: verum

end;

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

then j + 1 <= width G by A12, XXREAL_0:2;
then j < width G by NAT_1:13;
then A19: p `2 < (G * (1,(j + 1))) `2 by A15, GOBOARD6:28;
0 <> len G by MATRIX_0:def 10;
then A20: 1 <= len G by NAT_1:14;
j + 1 >= 1 by NAT_1:14;
then (G * (1,(j + 1))) `2 < (G * (1,j0)) `2 by A12, A18, A20, GOBOARD5:4;
hence contradiction by A8, A10, A13, A19; :: thesis: verum

end;

suppose A21: j0 = j + 1 ; :: thesis: contradiction

then j < width G by A12, NAT_1:13;
then p `2 < (G * (1,j0)) `2 by A15, A21, GOBOARD6:28;
hence contradiction by A8, A10, A13; :: thesis: verum

end;

end;

end;

hence contradiction by A6, A5, XBOOLE_0:def 4; :: thesis: verum

end;

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

then consider i0 being Nat such that
A22: 1 <= i0 and
A23: i0 <= len G and
A24: for p being Point of (TOP-REAL 2) st p in LSeg (f,k) holds
p `1 = (G * (i0,1)) `1 by A1, Th13;

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

A25: ( i0 > i implies i0 >= i + 1 ) by NAT_1:13;
assume A26: p in Int (v_strip (G,i)) ; :: thesis: contradiction

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

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

0 <> width G by MATRIX_0:def 10;
then 1 <= width G by NAT_1:14;
then A28: (G * (i,1)) `1 > (G * (i0,1)) `1 by A3, A22, A27, GOBOARD5:3;
i >= 1 by A22, A27, XXREAL_0:2;
then p `1 > (G * (i,1)) `1 by A3, A26, GOBOARD6:29;
hence contradiction by A8, A10, A24, A28; :: thesis: verum

end;

suppose i0 = i ; :: thesis: contradiction

then p `1 > (G * (i0,1)) `1 by A22, A23, A26, GOBOARD6:29;
hence contradiction by A8, A10, A24; :: thesis: verum

end;

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

then i + 1 <= len G by A23, XXREAL_0:2;
then i < len G by NAT_1:13;
then A30: p `1 < (G * ((i + 1),1)) `1 by A26, GOBOARD6:30;
0 <> width G by MATRIX_0:def 10;
then A31: 1 <= width G by NAT_1:14;
i + 1 >= 1 by NAT_1:14;
then (G * ((i + 1),1)) `1 < (G * (i0,1)) `1 by A23, A29, A31, GOBOARD5:3;
hence contradiction by A8, A10, A24, A30; :: thesis: verum

end;

suppose A32: i0 = i + 1 ; :: thesis: contradiction

then i < len G by A23, NAT_1:13;
then p `1 < (G * (i0,1)) `1 by A26, A32, GOBOARD6:30;
hence contradiction by A8, A10, A24; :: thesis: verum

end;

end;

end;

hence contradiction by A6, A5, XBOOLE_0:def 4; :: thesis: verum

end;

end;