let i1, i2, j1, j2 be Nat; :: thesis: for G1, G2 being Go-board st Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) holds
cell (G2,i2,j2) c= cell (G1,i1,j1)

let G1, G2 be Go-board; :: thesis: ( Values G1 c= Values G2 & [i1,j1] in Indices G1 & [i2,j2] in Indices G2 & G1 * (i1,j1) = G2 * (i2,j2) implies cell (G2,i2,j2) c= cell (G1,i1,j1) )
assume that
A1: Values G1 c= Values G2 and
A2: [i1,j1] in Indices G1 and
A3: [i2,j2] in Indices G2 and
A4: G1 * (i1,j1) = G2 * (i2,j2) ; :: thesis: cell (G2,i2,j2) c= cell (G1,i1,j1)
A5: 1 <= i1 by ;
A6: j1 <= width G1 by ;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in cell (G2,i2,j2) or p in cell (G1,i1,j1) )
assume A7: p in cell (G2,i2,j2) ; :: thesis: p in cell (G1,i1,j1)
A8: 1 <= i2 by ;
A9: j2 <= width G2 by ;
A10: 1 <= j2 by ;
A11: i2 <= len G2 by ;
then A12: ( (G2 * (i2,j2)) `1 = (G2 * (i2,1)) `1 & (G2 * (i2,j2)) `2 = (G2 * (1,j2)) `2 ) by ;
A13: 1 <= j1 by ;
A14: i1 <= len G1 by ;
then A15: ( (G1 * (i1,j1)) `1 = (G1 * (i1,1)) `1 & (G1 * (i1,j1)) `2 = (G1 * (1,j1)) `2 ) by ;
per cases ( ( i2 = len G2 & j2 = width G2 ) or ( i2 = len G2 & j2 < width G2 ) or ( i2 < len G2 & j2 = width G2 ) or ( i2 < len G2 & j2 < width G2 ) ) by ;
suppose A16: ( i2 = len G2 & j2 = width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then A17: p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & (G2 * (i2,j2)) `2 <= s ) } by ;
( i1 = len G1 & j1 = width G1 ) by A1, A2, A4, A8, A10, A16, Th3, Th5;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
suppose A18: ( i2 = len G2 & j2 < width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & (G2 * (i2,j2)) `2 <= s & s <= (G2 * (1,(j2 + 1))) `2 ) } by ;
then consider r9, s9 being Real such that
A19: ( p = |[r9,s9]| & (G2 * (i2,j2)) `1 <= r9 & (G2 * (i2,j2)) `2 <= s9 ) and
A20: s9 <= (G2 * (1,(j2 + 1))) `2 ;
A21: i1 = len G1 by A1, A2, A4, A10, A18, Th3;
now :: thesis: p in cell (G1,i1,j1)
per cases ( j1 = width G1 or j1 < width G1 ) by ;
suppose A22: j1 = width G1 ; :: thesis: p in cell (G1,i1,j1)
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s ) } by ;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
suppose A23: j1 < width G1 ; :: thesis: p in cell (G1,i1,j1)
( 1 <= j2 + 1 & j2 + 1 <= width G2 ) by ;
then A24: (G2 * (i2,(j2 + 1))) `2 = (G2 * (1,(j2 + 1))) `2 by ;
( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by ;
then ( G1 * (i1,(j1 + 1)) in Values G1 & (G1 * (i1,(j1 + 1))) `2 = (G1 * (1,(j1 + 1))) `2 ) by ;
then (G2 * (1,(j2 + 1))) `2 <= (G1 * (1,(j1 + 1))) `2 by A1, A4, A5, A14, A13, A8, A10, A18, A23, A24, Th8;
then s9 <= (G1 * (1,(j1 + 1))) `2 by ;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s & s <= (G1 * (1,(j1 + 1))) `2 ) } by ;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,j1) ; :: thesis: verum
end;
suppose A25: ( i2 < len G2 & j2 = width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & r <= (G2 * ((i2 + 1),1)) `1 & (G2 * (i2,j2)) `2 <= s ) } by ;
then consider r9, s9 being Real such that
A26: ( p = |[r9,s9]| & (G2 * (i2,j2)) `1 <= r9 ) and
A27: r9 <= (G2 * ((i2 + 1),1)) `1 and
A28: (G2 * (i2,j2)) `2 <= s9 ;
A29: j1 = width G1 by A1, A2, A4, A8, A25, Th5;
now :: thesis: p in cell (G1,i1,j1)
per cases ( i1 = len G1 or i1 < len G1 ) by ;
suppose A30: i1 = len G1 ; :: thesis: p in cell (G1,i1,j1)
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s ) } by A4, A26, A28;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
suppose A31: i1 < len G1 ; :: thesis: p in cell (G1,i1,j1)
( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by ;
then A32: (G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1 by ;
( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by ;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by ;
then (G2 * ((i2 + 1),1)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A6, A8, A10, A25, A31, A32, Th6;
then r9 <= (G1 * ((i1 + 1),1)) `1 by ;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (i1,j1)) `2 <= s ) } by A4, A26, A28;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,j1) ; :: thesis: verum
end;
suppose A33: ( i2 < len G2 & j2 < width G2 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= j2 + 1 & j2 + 1 <= width G2 ) by ;
then A34: (G2 * (i2,(j2 + 1))) `2 = (G2 * (1,(j2 + 1))) `2 by ;
( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by ;
then (G2 * ((i2 + 1),j2)) `1 = (G2 * ((i2 + 1),1)) `1 by ;
then p in { |[r,s]| where r, s is Real : ( (G2 * (i2,j2)) `1 <= r & r <= (G2 * ((i2 + 1),j2)) `1 & (G2 * (i2,j2)) `2 <= s & s <= (G2 * (i2,(j2 + 1))) `2 ) } by ;
then consider r9, s9 being Real such that
A35: ( p = |[r9,s9]| & (G2 * (i2,j2)) `1 <= r9 ) and
A36: r9 <= (G2 * ((i2 + 1),j2)) `1 and
A37: (G2 * (i2,j2)) `2 <= s9 and
A38: s9 <= (G2 * (i2,(j2 + 1))) `2 ;
now :: thesis: p in cell (G1,i1,j1)
per cases ( ( i1 = len G1 & j1 = width G1 ) or ( i1 = len G1 & j1 < width G1 ) or ( i1 < len G1 & j1 = width G1 ) or ( i1 < len G1 & j1 < width G1 ) ) by ;
suppose A39: ( i1 = len G1 & j1 = width G1 ) ; :: thesis: p in cell (G1,i1,j1)
p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s ) } by A4, A35, A37;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
suppose A40: ( i1 = len G1 & j1 < width G1 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by ;
then ( G1 * (i1,(j1 + 1)) in Values G1 & (G1 * (i1,(j1 + 1))) `2 = (G1 * (1,(j1 + 1))) `2 ) by ;
then (G2 * (i2,(j2 + 1))) `2 <= (G1 * (1,(j1 + 1))) `2 by A1, A4, A5, A13, A8, A10, A33, A40, Th8;
then s9 <= (G1 * (1,(j1 + 1))) `2 by ;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & (G1 * (i1,j1)) `2 <= s & s <= (G1 * (1,(j1 + 1))) `2 ) } by A4, A35, A37;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
suppose A41: ( i1 < len G1 & j1 = width G1 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by ;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by ;
then (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A8, A10, A33, A41, Th6;
then r9 <= (G1 * ((i1 + 1),1)) `1 by ;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,j1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (i1,j1)) `2 <= s ) } by A4, A35, A37;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
suppose A42: ( i1 < len G1 & j1 < width G1 ) ; :: thesis: p in cell (G1,i1,j1)
then ( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by ;
then (G1 * ((i1 + 1),j1)) `1 = (G1 * ((i1 + 1),1)) `1 by ;
then (G2 * ((i2 + 1),j2)) `1 <= (G1 * ((i1 + 1),1)) `1 by A1, A4, A5, A13, A8, A10, A33, A42, Th6;
then A43: r9 <= (G1 * ((i1 + 1),1)) `1 by ;
( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by ;
then ( G1 * (i1,(j1 + 1)) in Values G1 & (G1 * (i1,(j1 + 1))) `2 = (G1 * (1,(j1 + 1))) `2 ) by ;
then (G2 * (i2,(j2 + 1))) `2 <= (G1 * (1,(j1 + 1))) `2 by A1, A4, A5, A13, A8, A10, A33, A42, Th8;
then s9 <= (G1 * (1,(j1 + 1))) `2 by ;
then p in { |[r,s]| where r, s is Real : ( (G1 * (i1,1)) `1 <= r & r <= (G1 * ((i1 + 1),1)) `1 & (G1 * (1,j1)) `2 <= s & s <= (G1 * (1,(j1 + 1))) `2 ) } by A4, A15, A35, A37, A43;
hence p in cell (G1,i1,j1) by ; :: thesis: verum
end;
end;
end;
hence p in cell (G1,i1,j1) ; :: thesis: verum
end;
end;