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

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

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

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

now

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

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

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

then j >= 1 by A11, XXREAL_0:2;
then A16: p `2 > (G * 1,j) `2 by A4, A13, GOBOARD6:30;
0 <> len G by GOBOARD1:def 5;
then 1 <= len G by NAT_1:14;
then (G * 1,j) `2 > (G * 1,j0) `2 by A4, A11, A15, GOBOARD5:5;
hence contradiction by A7, A9, A12, A16; :: thesis: verum

end;

suppose j0 = j ; :: thesis: contradiction

then p `2 > (G * 1,j0) `2 by A11, A13, GOBOARD6:30;
hence contradiction by A7, A9, A12; :: thesis: verum

end;

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

then j + 1 <= width G by A11, XXREAL_0:2;
then j < width G by NAT_1:13;
then A18: p `2 < (G * 1,(j + 1)) `2 by A13, GOBOARD6:31;
0 <> len G by GOBOARD1:def 5;
then ( 1 <= len G & j + 1 >= 1 ) by NAT_1:14;
then (G * 1,(j + 1)) `2 < (G * 1,j0) `2 by A11, A17, GOBOARD5:5;
hence contradiction by A7, A9, A12, A18; :: thesis: verum

end;

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

then j < width G by A11, NAT_1:13;
then p `2 < (G * 1,j0) `2 by A13, A19, GOBOARD6:31;
hence contradiction by A7, A9, A12; :: thesis: verum

end;

end;

end;

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

end;

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

then consider i0 being Element of NAT such that
A20: ( 1 <= i0 & i0 <= len G ) and
A21: for p being Point of (TOP-REAL 2) st p in LSeg f,k holds
p `1 = (G * i0,1) `1 by A1, Th15;

now

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

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

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

then i >= 1 by A20, XXREAL_0:2;
then A25: p `1 > (G * i,1) `1 by A3, A22, GOBOARD6:32;
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by NAT_1:14;
then (G * i,1) `1 > (G * i0,1) `1 by A3, A20, A24, GOBOARD5:4;
hence contradiction by A7, A9, A21, A25; :: thesis: verum

end;

suppose i0 = i ; :: thesis: contradiction

then p `1 > (G * i0,1) `1 by A20, A22, GOBOARD6:32;
hence contradiction by A7, A9, A21; :: thesis: verum

end;

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

then i + 1 <= len G by A20, XXREAL_0:2;
then i < len G by NAT_1:13;
then A27: p `1 < (G * (i + 1),1) `1 by A22, GOBOARD6:33;
0 <> width G by GOBOARD1:def 5;
then ( 1 <= width G & i + 1 >= 1 ) by NAT_1:14;
then (G * (i + 1),1) `1 < (G * i0,1) `1 by A20, A26, GOBOARD5:4;
hence contradiction by A7, A9, A21, A27; :: thesis: verum

end;

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

then i < len G by A20, NAT_1:13;
then p `1 < (G * i0,1) `1 by A22, A28, GOBOARD6:33;
hence contradiction by A7, A9, A21; :: thesis: verum

end;

end;

end;

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

end;

end;