let i, j be 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))))
A4: 0 + 1 <= i + 1 by XREAL_1:6;
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 object ; :: 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, Th4;
A13: G * ((i + 1),j) = |[((G * ((i + 1),j)) `1),((G * ((i + 1),j)) `2)]| by EUCLID:53;
A14: j + 1 >= 1 by NAT_1:11;
(G * ((i + 1),j)) `1 = (G * ((i + 1),1)) `1 by A2, A3, A4, A5, Th2
.= (G * ((i + 1),(j + 1))) `1 by A4, A5, A11, A14, Th2 ;
then A15: G * ((i + 1),(j + 1)) = |[((G * ((i + 1),j)) `1),((G * ((i + 1),(j + 1))) `2)]| by EUCLID:53;
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, Th23;
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, Th2;
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, Th5;
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:52;
p `2 <= (G * ((i + 1),(j + 1))) `2 by A17, EUCLID:52;
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:9; :: thesis: verum

end;

A19: LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,i,j) by A1, A2, A3, Th18;
LSeg ((G * ((i + 1),j)),(G * ((i + 1),(j + 1)))) c= cell (G,(i + 1),j) by A2, A3, A4, A5, Th19;
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