let i, j be Element of NAT ; :: thesis: for G being Go-board st i < len G & 1 <= j & j < width G holds
(cell G,i,j) /\ (cell G,(i + 1),j) = LSeg (G * (i + 1),j),(G * (i + 1),(j + 1))
let G be Go-board; :: thesis: ( i < len G & 1 <= j & j < width G implies (cell G,i,j) /\ (cell G,(i + 1),j) = LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) )
assume that
A1: i < len G and
A2: 1 <= j and
A3: j < width G ; :: thesis: (cell G,i,j) /\ (cell G,(i + 1),j) = LSeg (G * (i + 1),j),(G * (i + 1),(j + 1))
0 <= i by NAT_1:2;
then A4: 0 + 1 <= i + 1 by XREAL_1:8;
A5: i + 1 <= len G by A1, NAT_1:13;
thus (cell G,i,j) /\ (cell G,(i + 1),j) c= LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) :: according to XBOOLE_0:def 10 :: thesis: LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= (cell G,i,j) /\ (cell G,(i + 1),j)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (cell G,i,j) /\ (cell G,(i + 1),j) or x in LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) )
A6: (cell G,i,j) /\ (cell G,(i + 1),j) = (v_strip G,i) /\ (((v_strip G,(i + 1)) /\ (h_strip G,j)) /\ (h_strip G,j)) by XBOOLE_1:16
.= (v_strip G,i) /\ ((v_strip G,(i + 1)) /\ ((h_strip G,j) /\ (h_strip G,j))) by XBOOLE_1:16
.= ((v_strip G,i) /\ (v_strip G,(i + 1))) /\ (h_strip G,j) by XBOOLE_1:16 ;
assume A7: x in (cell G,i,j) /\ (cell G,(i + 1),j) ; :: thesis: x in LSeg (G * (i + 1),j),(G * (i + 1),(j + 1))
then A8: x in (v_strip G,i) /\ (v_strip G,(i + 1)) by A6, XBOOLE_0:def 4;
A9: x in h_strip G,j by A6, A7, XBOOLE_0:def 4;
A10: j < j + 1 by NAT_1:13;
A11: j + 1 <= width G by A3, NAT_1:13;
then A12: (G * (i + 1),j) `2 < (G * (i + 1),(j + 1)) `2 by A2, A4, A5, A10, Th5;
A13: G * (i + 1),j = |[((G * (i + 1),j) `1 ),((G * (i + 1),j) `2 )]| by EUCLID:57;
A14: j + 1 >= 1 by NAT_1:11;
(G * (i + 1),j) `1 = (G * (i + 1),1) `1 by A2, A3, A4, A5, Th3
.= (G * (i + 1),(j + 1)) `1 by A4, A5, A11, A14, Th3 ;
then A15: G * (i + 1),(j + 1) = |[((G * (i + 1),j) `1 ),((G * (i + 1),(j + 1)) `2 )]| by EUCLID:57;
reconsider p = x as Point of (TOP-REAL 2) by A7;
i + 1 <= len G by A1, NAT_1:13;
then p in { q where q is Point of (TOP-REAL 2) : q `1 = (G * (i + 1),1) `1 } by A8, Th24;
then ex q being Point of (TOP-REAL 2) st
( q = p & q `1 = (G * (i + 1),1) `1 ) ;
then A16: p `1 = (G * (i + 1),j) `1 by A2, A3, A4, A5, Th3;
p in { |[r,s]| where r, s is Real : ( (G * (i + 1),j) `2 <= s & s <= (G * (i + 1),(j + 1)) `2 ) } by A2, A3, A4, A5, A9, Th6;
then A17: ex r, s being Real st
( p = |[r,s]| & (G * (i + 1),j) `2 <= s & s <= (G * (i + 1),(j + 1)) `2 ) ;
then A18: (G * (i + 1),j) `2 <= p `2 by EUCLID:56;
p `2 <= (G * (i + 1),(j + 1)) `2 by A17, EUCLID:56;
then p in { q where q is Point of (TOP-REAL 2) : ( q `1 = (G * (i + 1),j) `1 & (G * (i + 1),j) `2 <= q `2 & q `2 <= (G * (i + 1),(j + 1)) `2 ) } by A16, A18;
hence x in LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) by A12, A13, A15, TOPREAL3:15; :: thesis: verum

end;

A19: LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= cell G,i,j by A1, A2, A3, Th19;
LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= cell G,(i + 1),j by A2, A3, A4, A5, Th20;
hence LSeg (G * (i + 1),j),(G * (i + 1),(j + 1)) c= (cell G,i,j) /\ (cell G,(i + 1),j) by A19, XBOOLE_1:19; :: thesis: verum