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

proof

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

end;

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