let j, i be Element of 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))
0 <= j by NAT_1:2;
then A4: 0 + 1 <= j + 1 by XREAL_1:8;
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 set ; :: 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, Th4;
A13: G * i,(j + 1) = |[((G * i,(j + 1)) `1 ),((G * i,(j + 1)) `2 )]| by EUCLID:57;
A14: i + 1 >= 1 by NAT_1:11;
(G * i,(j + 1)) `2 = (G * 1,(j + 1)) `2 by A2, A3, A4, A5, Th2
.= (G * (i + 1),(j + 1)) `2 by A4, A5, A11, A14, Th2 ;
then A15: G * (i + 1),(j + 1) = |[((G * (i + 1),(j + 1)) `1 ),((G * i,(j + 1)) `2 )]| by EUCLID:57;
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, Th25;
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, Th2;
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, Th9;
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:56;
p `1 <= (G * (i + 1),(j + 1)) `1 by A17, EUCLID:56;
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:16; :: thesis: verum

end;

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