let i1, j1, i2, j2 be Element of 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 A2, MATRIX_1:39;
A6: j1 <= width G1 by A2, MATRIX_1:39;
let p be set ; :: 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 A3, MATRIX_1:39;
A9: j2 <= width G2 by A3, MATRIX_1:39;
A10: 1 <= j2 by A3, MATRIX_1:39;
A11: i2 <= len G2 by A3, MATRIX_1:39;
then A12: ( (G2 * i2,j2) `1 = (G2 * i2,1) `1 & (G2 * i2,j2) `2 = (G2 * 1,j2) `2 ) by A8, A10, A9, GOBOARD5:2, GOBOARD5:3;
A13: 1 <= j1 by A2, MATRIX_1:39;
A14: i1 <= len G1 by A2, MATRIX_1:39;
then A15: ( (G1 * i1,j1) `1 = (G1 * i1,1) `1 & (G1 * i1,j1) `2 = (G1 * 1,j1) `2 ) by A5, A13, A6, GOBOARD5:2, GOBOARD5:3;

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 A11, A9, XXREAL_0:1;

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 A7, A12, GOBRD11:28;
( i1 = len G1 & j1 = width G1 ) by A1, A2, A4, A8, A10, A16, Th11, Th13;
hence p in cell G1,i1,j1 by A4, A15, A17, GOBRD11:28; :: 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 A7, A10, A12, GOBRD11:29;
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, Th11;

now

per cases ( j1 = width G1 or j1 < width G1 ) by A6, XXREAL_0:1;

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 A4, A19;
hence p in cell G1,i1,j1 by A15, A21, A22, GOBRD11:28; :: thesis: verum

end;

suppose A23: j1 < width G1 ; :: thesis: p in cell G1,i1,j1

( 1 <= j2 + 1 & j2 + 1 <= width G2 ) by A18, NAT_1:12, NAT_1:13;
then A24: (G2 * i2,(j2 + 1)) `2 = (G2 * 1,(j2 + 1)) `2 by A8, A11, GOBOARD5:2;
( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by A23, NAT_1:12, NAT_1:13;
then ( G1 * i1,(j1 + 1) in Values G1 & (G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 ) by A5, A14, Lm1, GOBOARD5:2;
then (G2 * 1,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2 by A1, A4, A5, A14, A13, A8, A10, A18, A23, A24, Th16;
then s9 <= (G1 * 1,(j1 + 1)) `2 by A20, XXREAL_0:2;
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, A19;
hence p in cell G1,i1,j1 by A13, A15, A21, A23, GOBRD11:29; :: 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 A7, A8, A12, GOBRD11:31;
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, Th13;

now

per cases ( i1 = len G1 or i1 < len G1 ) by A14, XXREAL_0:1;

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 A15, A29, A30, GOBRD11:28; :: thesis: verum

end;

suppose A31: i1 < len G1 ; :: thesis: p in cell G1,i1,j1

( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A25, NAT_1:12, NAT_1:13;
then A32: (G2 * (i2 + 1),j2) `1 = (G2 * (i2 + 1),1) `1 by A10, A9, GOBOARD5:3;
( 1 <= i1 + 1 & i1 + 1 <= len G1 ) by A31, NAT_1:12, NAT_1:13;
then (G1 * (i1 + 1),j1) `1 = (G1 * (i1 + 1),1) `1 by A13, A6, GOBOARD5:3;
then (G2 * (i2 + 1),1) `1 <= (G1 * (i1 + 1),1) `1 by A1, A4, A5, A13, A6, A8, A10, A25, A31, A32, Th14;
then r9 <= (G1 * (i1 + 1),1) `1 by A27, XXREAL_0:2;
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 A5, A15, A29, A31, GOBRD11:31; :: 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 NAT_1:12, NAT_1:13;
then A34: (G2 * i2,(j2 + 1)) `2 = (G2 * 1,(j2 + 1)) `2 by A8, A11, GOBOARD5:2;
( 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A33, NAT_1:12, NAT_1:13;
then (G2 * (i2 + 1),j2) `1 = (G2 * (i2 + 1),1) `1 by A10, A9, GOBOARD5:3;
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 A7, A8, A10, A12, A33, A34, GOBRD11:32;
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

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 A14, A6, XXREAL_0:1;

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 A15, A39, GOBRD11:28; :: 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 NAT_1:12, NAT_1:13;
then ( G1 * i1,(j1 + 1) in Values G1 & (G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 ) by A5, A14, Lm1, GOBOARD5:2;
then (G2 * i2,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2 by A1, A4, A5, A13, A8, A10, A33, A40, Th16;
then s9 <= (G1 * 1,(j1 + 1)) `2 by A38, XXREAL_0:2;
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 A13, A15, A40, GOBRD11:29; :: 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 NAT_1:12, NAT_1:13;
then (G1 * (i1 + 1),j1) `1 = (G1 * (i1 + 1),1) `1 by A13, A6, GOBOARD5:3;
then (G2 * (i2 + 1),j2) `1 <= (G1 * (i1 + 1),1) `1 by A1, A4, A5, A13, A8, A10, A33, A41, Th14;
then r9 <= (G1 * (i1 + 1),1) `1 by A36, XXREAL_0:2;
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 A5, A15, A41, GOBRD11:31; :: 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 NAT_1:12, NAT_1:13;
then (G1 * (i1 + 1),j1) `1 = (G1 * (i1 + 1),1) `1 by A13, A6, GOBOARD5:3;
then (G2 * (i2 + 1),j2) `1 <= (G1 * (i1 + 1),1) `1 by A1, A4, A5, A13, A8, A10, A33, A42, Th14;
then A43: r9 <= (G1 * (i1 + 1),1) `1 by A36, XXREAL_0:2;
( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by A42, NAT_1:12, NAT_1:13;
then ( G1 * i1,(j1 + 1) in Values G1 & (G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 ) by A5, A14, Lm1, GOBOARD5:2;
then (G2 * i2,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2 by A1, A4, A5, A13, A8, A10, A33, A42, Th16;
then s9 <= (G1 * 1,(j1 + 1)) `2 by A38, XXREAL_0:2;
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 A5, A13, A42, GOBRD11:32; :: thesis: verum

end;

end;

end;

hence p in cell G1,i1,j1 ; :: thesis: verum

end;

end;