let i be Element of 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 ) } )
assume A1: ( 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 ) }
0 <> width G by GOBOARD1:def 5;
then 1 <= width G by NAT_1:14;
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:9;
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 set ; :: 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 Lm5;
consider r1 being real number such that
A4: r1 > 0 and
A5: Ball u,r1 c= v_strip G,i by A3, Th8;
reconsider r1 = r1 as Real by XREAL_0:def 1;
reconsider p = u as Point of (TOP-REAL 2) by Lm5;
set q1 = |[((p `1 ) + (r1 / 2)),((p `2 ) + 0 )]|;
A6: p = |[(p `1 ),(p `2 )]| by EUCLID:57;
A7: ( r1 / 2 > 0 & r1 / 2 < r1 ) by A4, XREAL_1:217, XREAL_1:218;
then |[((p `1 ) + (r1 / 2)),((p `2 ) + 0 )]| in Ball u,r1 by A6, Th10;
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 A8: (p `1 ) + (r1 / 2) <= (G * (i + 1),1) `1 by SPPOL_2:1;
p `1 < (p `1 ) + (r1 / 2) by A7, XREAL_1:31;
then A9: p `1 < (G * (i + 1),1) `1 by A8, XXREAL_0:2;
set q2 = |[((p `1 ) - (r1 / 2)),((p `2 ) + 0 )]|;
|[((p `1 ) - (r1 / 2)),((p `2 ) + 0 )]| in Ball u,r1 by A6, A7, Th12;
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 A10: ((G * i,1) `1 ) + (r1 / 2) <= p `1 by XREAL_1:21;
(G * i,1) `1 < ((G * i,1) `1 ) + (r1 / 2) by A7, XREAL_1:31;
then (G * i,1) `1 < p `1 by A10, 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, A9; :: thesis: verum

end;

let x be set ; :: 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:13;
A14: ((G * (i + 1),1) `1 ) - r > 0 by A13, XREAL_1:52;
r - ((G * i,1) `1 ) > 0 by A12, XREAL_1:52;
then min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r) > 0 by A14, XXREAL_0:15;
then A15: u in Ball u,(min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r)) by Th4;
A16: Ball u,(min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r)) c= v_strip G,i

proof

let y be set ; :: 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 )
A17: 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:18;
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
A18: v = y and
A19: dist u,v < min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r) by A17;
reconsider q = v as Point of (TOP-REAL 2) by TOPREAL3:13;
A20: q = |[(q `1 ),(q `2 )]| by EUCLID:57;
then A21: sqrt (((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 )) < min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r) by A19, Th9;
A22: (r - (q `1 )) ^2 >= 0 by XREAL_1:65;
0 <= (s - (q `2 )) ^2 by XREAL_1:65;
then ((r - (q `1 )) ^2 ) + 0 <= ((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 ) by XREAL_1:8;
then sqrt ((r - (q `1 )) ^2 ) <= sqrt (((r - (q `1 )) ^2 ) + ((s - (q `2 )) ^2 )) by A22, SQUARE_1:94;
then sqrt ((r - (q `1 )) ^2 ) <= min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r) by A21, XXREAL_0:2;
then abs (r - (q `1 )) <= min (r - ((G * i,1) `1 )),(((G * (i + 1),1) `1 ) - r) by COMPLEX1:158;
then A23: ( abs (r - (q `1 )) <= r - ((G * i,1) `1 ) & abs (r - (q `1 )) <= ((G * (i + 1),1) `1 ) - r ) by 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:50;
abs (r - (q `1 )) = abs (- (r - (q `1 ))) by COMPLEX1:138
.= (q `1 ) - r by A25, ABSVALUE:def 1 ;
then A26: q `1 <= (G * (i + 1),1) `1 by A23, XREAL_1:11;
(G * i,1) `1 <= q `1 by A12, A24, XXREAL_0:2;
hence y in v_strip G,i by A2, A18, 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:50;
then abs (r - (q `1 )) = r - (q `1 ) by ABSVALUE:def 1;
then A28: (G * i,1) `1 <= q `1 by A23, XREAL_1:12;
q `1 <= (G * (i + 1),1) `1 by A13, A27, XXREAL_0:2;
hence y in v_strip G,i by A2, A18, 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:13;
B is open by Th6;
hence x in Int (v_strip G,i) by A11, A15, A16, TOPS_1:54; :: thesis: verum