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
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 A5: p in cell G2,i2,j2 ; :: thesis: p in cell G1,i1,j1
A6: ( 1 <= i1 & i1 <= len G1 & 1 <= j1 & j1 <= width G1 ) by A2, MATRIX_1:39;
A7: ( 1 <= i2 & i2 <= len G2 & 1 <= j2 & j2 <= width G2 ) by A3, MATRIX_1:39;
A8: ( (G1 * i1,j1) `1 = (G1 * i1,1) `1 & (G1 * i1,j1) `2 = (G1 * 1,j1) `2 ) by A6, GOBOARD5:2, GOBOARD5:3;
A9: ( (G2 * i2,j2) `1 = (G2 * i2,1) `1 & (G2 * i2,j2) `2 = (G2 * 1,j2) `2 ) by A7, 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 A7, XXREAL_0:1;

suppose A10: ( i2 = len G2 & j2 = width G2 ) ; :: thesis: p in cell G1,i1,j1

then A11: ( i1 = len G1 & j1 = width G1 ) by A1, A2, A4, A7, Th11, Th13;
p in { |[r,s]| where r, s is Real : ( (G2 * i2,j2) `1 <= r & (G2 * i2,j2) `2 <= s ) } by A5, A9, A10, GOBRD11:28;
hence p in cell G1,i1,j1 by A4, A8, A11, GOBRD11:28; :: thesis: verum

end;

suppose A12: ( i2 = len G2 & j2 < width G2 ) ; :: thesis: p in cell G1,i1,j1

then A13: i1 = len G1 by A1, A2, A4, A7, Th11;
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 A5, A7, A9, A12, GOBRD11:29;
then consider r', s' being Real such that
A14: p = |[r',s']| and
A15: ( (G2 * i2,j2) `1 <= r' & (G2 * i2,j2) `2 <= s' ) and
A16: s' <= (G2 * 1,(j2 + 1)) `2 ;

now

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

suppose A17: 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, A14, A15;
hence p in cell G1,i1,j1 by A8, A13, A17, GOBRD11:28; :: thesis: verum

end;

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

then A19: ( 1 <= j1 + 1 & j1 + 1 <= width G1 & 1 <= j2 + 1 & j2 + 1 <= width G2 ) by A12, NAT_1:12, NAT_1:13;
then A20: G1 * i1,(j1 + 1) in Values G1 by A6, Lm1;
( (G2 * i2,(j2 + 1)) `2 = (G2 * 1,(j2 + 1)) `2 & (G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 ) by A6, A7, A19, GOBOARD5:2;
then (G2 * 1,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2 by A1, A4, A6, A7, A12, A18, A20, Th16;
then s' <= (G1 * 1,(j1 + 1)) `2 by A16, 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, A14, A15;
hence p in cell G1,i1,j1 by A6, A8, A13, A18, GOBRD11:29; :: thesis: verum

end;

end;

end;

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

end;

suppose A21: ( i2 < len G2 & j2 = width G2 ) ; :: thesis: p in cell G1,i1,j1

then A22: j1 = width G1 by A1, A2, A4, A7, Th13;
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 A5, A7, A9, A21, GOBRD11:31;
then consider r', s' being Real such that
A23: p = |[r',s']| and
A24: (G2 * i2,j2) `1 <= r' and
A25: r' <= (G2 * (i2 + 1),1) `1 and
A26: (G2 * i2,j2) `2 <= s' ;

now

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

suppose A27: 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, A23, A24, A26;
hence p in cell G1,i1,j1 by A8, A22, A27, GOBRD11:28; :: thesis: verum

end;

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

then ( 1 <= i1 + 1 & i1 + 1 <= len G1 & 1 <= i2 + 1 & i2 + 1 <= len G2 ) by A21, NAT_1:12, NAT_1:13;
then ( (G2 * (i2 + 1),j2) `1 = (G2 * (i2 + 1),1) `1 & (G1 * (i1 + 1),j1) `1 = (G1 * (i1 + 1),1) `1 ) by A6, A7, GOBOARD5:3;
then (G2 * (i2 + 1),1) `1 <= (G1 * (i1 + 1),1) `1 by A1, A4, A6, A7, A21, A28, Th14;
then r' <= (G1 * (i1 + 1),1) `1 by A25, 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, A23, A24, A26;
hence p in cell G1,i1,j1 by A6, A8, A22, A28, GOBRD11:31; :: thesis: verum

end;

end;

end;

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

end;

suppose A29: ( i2 < len G2 & j2 < width G2 ) ; :: thesis: p in cell G1,i1,j1

then ( 1 <= i2 + 1 & i2 + 1 <= len G2 & 1 <= j2 + 1 & j2 + 1 <= width G2 ) by NAT_1:12, NAT_1:13;
then ( (G2 * (i2 + 1),j2) `1 = (G2 * (i2 + 1),1) `1 & (G2 * i2,(j2 + 1)) `2 = (G2 * 1,(j2 + 1)) `2 ) by A7, GOBOARD5:2, 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 A5, A7, A9, A29, GOBRD11:32;
then consider r', s' being Real such that
A30: p = |[r',s']| and
A31: (G2 * i2,j2) `1 <= r' and
A32: r' <= (G2 * (i2 + 1),j2) `1 and
A33: (G2 * i2,j2) `2 <= s' and
A34: s' <= (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 A6, XXREAL_0:1;

suppose A35: ( 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, A30, A31, A33;
hence p in cell G1,i1,j1 by A8, A35, GOBRD11:28; :: thesis: verum

end;

suppose A36: ( i1 = len G1 & j1 < width G1 ) ; :: thesis: p in cell G1,i1,j1

then A37: ( 1 <= j1 + 1 & j1 + 1 <= width G1 ) by NAT_1:12, NAT_1:13;
then A38: G1 * i1,(j1 + 1) in Values G1 by A6, Lm1;
(G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 by A6, A37, GOBOARD5:2;
then (G2 * i2,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2 by A1, A4, A6, A7, A29, A36, A38, Th16;
then s' <= (G1 * 1,(j1 + 1)) `2 by A34, 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, A30, A31, A33;
hence p in cell G1,i1,j1 by A6, A8, A36, GOBRD11:29; :: thesis: verum

end;

suppose A39: ( 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 A6, GOBOARD5:3;
then (G2 * (i2 + 1),j2) `1 <= (G1 * (i1 + 1),1) `1 by A1, A4, A6, A7, A29, A39, Th14;
then r' <= (G1 * (i1 + 1),1) `1 by A32, 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, A30, A31, A33;
hence p in cell G1,i1,j1 by A6, A8, A39, GOBRD11:31; :: thesis: verum

end;

suppose A40: ( i1 < len G1 & j1 < width G1 ) ; :: thesis: p in cell G1,i1,j1

then A41: ( 1 <= j1 + 1 & j1 + 1 <= width G1 & 1 <= i1 + 1 & i1 + 1 <= len G1 ) by NAT_1:12, NAT_1:13;
then A42: G1 * i1,(j1 + 1) in Values G1 by A6, Lm1;
( (G1 * i1,(j1 + 1)) `2 = (G1 * 1,(j1 + 1)) `2 & (G1 * (i1 + 1),j1) `1 = (G1 * (i1 + 1),1) `1 ) by A6, A41, GOBOARD5:2, GOBOARD5:3;
then ( (G2 * i2,(j2 + 1)) `2 <= (G1 * 1,(j1 + 1)) `2 & (G2 * (i2 + 1),j2) `1 <= (G1 * (i1 + 1),1) `1 ) by A1, A4, A6, A7, A29, A40, A42, Th14, Th16;
then ( s' <= (G1 * 1,(j1 + 1)) `2 & r' <= (G1 * (i1 + 1),1) `1 ) by A32, A34, 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, A8, A30, A31, A33;
hence p in cell G1,i1,j1 by A6, A40, GOBRD11:32; :: thesis: verum

end;

end;

end;

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

end;

end;