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 Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) `
let f be FinSequence of (TOP-REAL 2); :: thesis: ( f is_sequence_on G & f is special implies for i, j being Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) ` )
assume that
A1: f is_sequence_on G and
A2: f is special ; :: thesis: for i, j being Element of NAT st i <= len G & j <= width G holds
Int (cell (G,i,j)) c= (L~ f) `
let i, j be Element of NAT ; :: thesis: ( i <= len G & j <= width G implies Int (cell (G,i,j)) c= (L~ f) ` )
assume that
A3: i <= len G and
A4: j <= width G ; :: thesis: Int (cell (G,i,j)) c= (L~ f) `
Int (cell (G,i,j)) misses L~ f by A1, A2, A3, A4, JORDAN9:16;
hence Int (cell (G,i,j)) c= (L~ f) ` by SUBSET_1:43; :: thesis: verum