let i be Nat; :: thesis: for G being Go-board st 1 <= i & i < len G holds
Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) }
let G be Go-board; :: thesis: ( 1 <= i & i < len G implies Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } )
0 <> width G by MATRIX_0:def 10;
then A1: 1 <= width G by NAT_1:14;
assume ( 1 <= i & i < len G ) ; :: thesis: Int (v_strip (G,i)) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) }
then A2: v_strip (G,i) = { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 <= r & r <= (G * ((i + 1),1)) `1 ) } by A1, GOBOARD5:8;
thus Int (v_strip (G,i)) c= { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } :: according to XBOOLE_0:def 10 :: thesis: { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } c= Int (v_strip (G,i))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Int (v_strip (G,i)) or x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } )
assume A3: x in Int (v_strip (G,i)) ; :: thesis: x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) }
then reconsider u = x as Point of (Euclid 2) by Lm6;
consider r1 being Real such that
A4: r1 > 0 and
A5: Ball (u,r1) c= v_strip (G,i) by A3, Th5;
reconsider p = u as Point of (TOP-REAL 2) by Lm6;
A6: p = |[(p `1),(p `2)]| by EUCLID:53;
set q2 = |[((p `1) - (r1 / 2)),((p `2) + 0)]|;
A7: r1 / 2 < r1 by A4, XREAL_1:216;
then |[((p `1) - (r1 / 2)),((p `2) + 0)]| in Ball (u,r1) by A4, A6, Th9;
then |[((p `1) - (r1 / 2)),((p `2) + 0)]| in v_strip (G,i) by A5;
then ex r2, s2 being Real st
( |[((p `1) - (r1 / 2)),((p `2) + 0)]| = |[r2,s2]| & (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 ) by A2;
then (G * (i,1)) `1 <= (p `1) - (r1 / 2) by SPPOL_2:1;
then A8: ((G * (i,1)) `1) + (r1 / 2) <= p `1 by XREAL_1:19;
set q1 = |[((p `1) + (r1 / 2)),((p `2) + 0)]|;
|[((p `1) + (r1 / 2)),((p `2) + 0)]| in Ball (u,r1) by A4, A6, A7, Th7;
then |[((p `1) + (r1 / 2)),((p `2) + 0)]| in v_strip (G,i) by A5;
then ex r2, s2 being Real st
( |[((p `1) + (r1 / 2)),((p `2) + 0)]| = |[r2,s2]| & (G * (i,1)) `1 <= r2 & r2 <= (G * ((i + 1),1)) `1 ) by A2;
then A9: (p `1) + (r1 / 2) <= (G * ((i + 1),1)) `1 by SPPOL_2:1;
(G * (i,1)) `1 < ((G * (i,1)) `1) + (r1 / 2) by A4, XREAL_1:29, XREAL_1:215;
then A10: (G * (i,1)) `1 < p `1 by A8, XXREAL_0:2;
p `1 < (p `1) + (r1 / 2) by A4, XREAL_1:29, XREAL_1:215;
then p `1 < (G * ((i + 1),1)) `1 by A9, XXREAL_0:2;
hence x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } by A6, A10; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } or x in Int (v_strip (G,i)) )
assume x in { |[r,s]| where r, s is Real : ( (G * (i,1)) `1 < r & r < (G * ((i + 1),1)) `1 ) } ; :: thesis: x in Int (v_strip (G,i))
then consider r, s being Real such that
A11: x = |[r,s]| and
A12: (G * (i,1)) `1 < r and
A13: r < (G * ((i + 1),1)) `1 ;
reconsider u = |[r,s]| as Point of (Euclid 2) by TOPREAL3:8;
( ((G * ((i + 1),1)) `1) - r > 0 & r - ((G * (i,1)) `1) > 0 ) by A12, A13, XREAL_1:50;
then min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)) > 0 by XXREAL_0:15;
then A14: u in Ball (u,(min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)))) by Th1;
A15: Ball (u,(min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)))) c= v_strip (G,i)

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball (u,(min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)))) or y in v_strip (G,i) )
A16: Ball (u,(min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)))) = { v where v is Point of (Euclid 2) : dist (u,v) < min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)) } by METRIC_1:17;
assume y in Ball (u,(min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)))) ; :: thesis: y in v_strip (G,i)
then consider v being Point of (Euclid 2) such that
A17: v = y and
A18: dist (u,v) < min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)) by A16;
reconsider q = v as Point of (TOP-REAL 2) by TOPREAL3:8;
( (r - (q `1)) ^2 >= 0 & ((r - (q `1)) ^2) + 0 <= ((r - (q `1)) ^2) + ((s - (q `2)) ^2) ) by XREAL_1:6, XREAL_1:63;
then A19: sqrt ((r - (q `1)) ^2) <= sqrt (((r - (q `1)) ^2) + ((s - (q `2)) ^2)) by SQUARE_1:26;
A20: q = |[(q `1),(q `2)]| by EUCLID:53;
then sqrt (((r - (q `1)) ^2) + ((s - (q `2)) ^2)) < min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)) by A18, Th6;
then sqrt ((r - (q `1)) ^2) <= min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)) by A19, XXREAL_0:2;
then A21: |.(r - (q `1)).| <= min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)) by COMPLEX1:72;
then A22: |.(r - (q `1)).| <= r - ((G * (i,1)) `1) by XXREAL_0:22;
A23: |.(r - (q `1)).| <= ((G * ((i + 1),1)) `1) - r by A21, XXREAL_0:22;

per cases ( r <= q `1 or r >= q `1 ) ;

suppose A24: r <= q `1 ; :: thesis: y in v_strip (G,i)

then A25: (q `1) - r >= 0 by XREAL_1:48;
|.(r - (q `1)).| = |.(- (r - (q `1))).| by COMPLEX1:52
.= (q `1) - r by A25, ABSVALUE:def 1 ;
then A26: q `1 <= (G * ((i + 1),1)) `1 by A23, XREAL_1:9;
(G * (i,1)) `1 <= q `1 by A12, A24, XXREAL_0:2;
hence y in v_strip (G,i) by A2, A17, A20, A26; :: thesis: verum

end;

suppose A27: r >= q `1 ; :: thesis: y in v_strip (G,i)

then r - (q `1) >= 0 by XREAL_1:48;
then |.(r - (q `1)).| = r - (q `1) by ABSVALUE:def 1;
then A28: (G * (i,1)) `1 <= q `1 by A22, XREAL_1:10;
q `1 <= (G * ((i + 1),1)) `1 by A13, A27, XXREAL_0:2;
hence y in v_strip (G,i) by A2, A17, A20, A28; :: thesis: verum

end;

end;

end;

reconsider B = Ball (u,(min ((r - ((G * (i,1)) `1)),(((G * ((i + 1),1)) `1) - r)))) as Subset of (TOP-REAL 2) by TOPREAL3:8;
B is open by Th3;
hence x in Int (v_strip (G,i)) by A11, A14, A15, TOPS_1:22; :: thesis: verum