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;