let f be non constant standard special_circular_sequence; :: thesis: the carrier of (TOP-REAL 2) = union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }

set j1 = len (GoB f);

set j2 = width (GoB f);

thus the carrier of (TOP-REAL 2) c= union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } :: according to XBOOLE_0:def 10 :: thesis: union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } c= the carrier of (TOP-REAL 2)

assume x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } ; :: thesis: x in the carrier of (TOP-REAL 2)

then consider X0 being set such that

A48: ( x in X0 & X0 in { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by TARSKI:def 4;

ex i, j being Nat st

( X0 = cell ((GoB f),i,j) & i <= len (GoB f) & j <= width (GoB f) ) by A48;

hence x in the carrier of (TOP-REAL 2) by A48; :: thesis: verum

set j1 = len (GoB f);

set j2 = width (GoB f);

thus the carrier of (TOP-REAL 2) c= union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } :: according to XBOOLE_0:def 10 :: thesis: union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } c= the carrier of (TOP-REAL 2)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in the carrier of (TOP-REAL 2) )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (TOP-REAL 2) or x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } )

assume x in the carrier of (TOP-REAL 2) ; :: thesis: x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }

then reconsider p = x as Point of (TOP-REAL 2) ;

set r = p `1 ;

A22: j0 <= len (GoB f) and

A23: x in v_strip ((GoB f),j0) ;

set s = p `2 ;

A45: i0 <= width (GoB f) and

A46: x in h_strip ((GoB f),i0) ;

reconsider X0 = cell ((GoB f),j0,i0) as set ;

x in (v_strip ((GoB f),j0)) /\ (h_strip ((GoB f),i0)) by A23, A46, XBOOLE_0:def 4;

then A47: x in X0 by GOBOARD5:def 3;

X0 in { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } by A22, A45;

hence x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } by A47, TARSKI:def 4; :: thesis: verum

end;assume x in the carrier of (TOP-REAL 2) ; :: thesis: x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) }

then reconsider p = x as Point of (TOP-REAL 2) ;

set r = p `1 ;

A1: now :: thesis: ( not p `1 < ((GoB f) * (1,1)) `1 & not ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 implies ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) )

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) )

assume that

A2: not p `1 < ((GoB f) * (1,1)) `1 and

A3: not ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 ; :: thesis: ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 )

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; :: thesis: verum

end;A2: not p `1 < ((GoB f) * (1,1)) `1 and

A3: not ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 ; :: thesis: ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 )

now :: thesis: ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 )

hence
ex j being Nat st ( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 )

reconsider l = len (GoB f) as Nat ;

defpred S_{1}[ Nat] means not ( not $1 = 0 & 1 <= $1 & $1 < len (GoB f) & not ((GoB f) * (($1 + 1),1)) `1 <= p `1 );

1 < len (GoB f) by GOBOARD7:32;

then 1 + 1 <= len (GoB f) by NAT_1:13;

then A4: (1 + 1) - 1 <= l - 1 by XREAL_1:9;

assume A5: for j being Nat holds

( not 1 <= j or not j < len (GoB f) or not ((GoB f) * (j,1)) `1 <= p `1 or not p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; :: thesis: contradiction

A6: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A11: for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A10, A6);

A12: l - 1 < (l - 1) + 1 by XREAL_1:29;

then reconsider l1 = l - 1 as Nat by A4, SPPOL_1:2;

0 < l1 by A4;

hence contradiction by A3, A11, A4, A12; :: thesis: verum

end;defpred S

1 < len (GoB f) by GOBOARD7:32;

then 1 + 1 <= len (GoB f) by NAT_1:13;

then A4: (1 + 1) - 1 <= l - 1 by XREAL_1:9;

assume A5: for j being Nat holds

( not 1 <= j or not j < len (GoB f) or not ((GoB f) * (j,1)) `1 <= p `1 or not p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; :: thesis: contradiction

A6: for k being Nat st S

S

proof

A10:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A7: not ( not k = 0 & 1 <= k & k < len (GoB f) & not ((GoB f) * ((k + 1),1)) `1 <= p `1 ) ; :: thesis: S_{1}[k + 1]

( 1 <= k + 1 & k + 1 < len (GoB f) implies ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 )_{1}[k + 1]
; :: thesis: verum

end;assume A7: not ( not k = 0 & 1 <= k & k < len (GoB f) & not ((GoB f) * ((k + 1),1)) `1 <= p `1 ) ; :: thesis: S

( 1 <= k + 1 & k + 1 < len (GoB f) implies ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 )

proof

hence
S
assume A8:
( 1 <= k + 1 & k + 1 < len (GoB f) )
; :: thesis: ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1

end;now :: thesis: not p `1 < ((GoB f) * (((k + 1) + 1),1)) `1

hence
((GoB f) * (((k + 1) + 1),1)) `1 <= p `1
; :: thesis: verumassume A9:
p `1 < ((GoB f) * (((k + 1) + 1),1)) `1
; :: thesis: contradiction

then k <> 0 by A2, A5, GOBOARD7:32;

then 0 + 1 <= k by NAT_1:13;

hence contradiction by A5, A7, A8, A9, XREAL_1:145; :: thesis: verum

end;then k <> 0 by A2, A5, GOBOARD7:32;

then 0 + 1 <= k by NAT_1:13;

hence contradiction by A5, A7, A8, A9, XREAL_1:145; :: thesis: verum

A11: for j being Nat holds S

A12: l - 1 < (l - 1) + 1 by XREAL_1:29;

then reconsider l1 = l - 1 as Nat by A4, SPPOL_1:2;

0 < l1 by A4;

hence contradiction by A3, A11, A4, A12; :: thesis: verum

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; :: thesis: verum

now :: thesis: ( ( p `1 < ((GoB f) * (1,1)) `1 & ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ) or ( ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 & ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ) or ( ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) & ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ) )end;

then consider j0 being Nat such that ( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ) or ( ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 & ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ) or ( ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) & ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ) )

per cases
( p `1 < ((GoB f) * (1,1)) `1 or ((GoB f) * ((len (GoB f)),1)) `1 <= p `1 or ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ) by A1;

end;

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ) by A1;

case A13:
p `1 < ((GoB f) * (1,1)) `1
; :: thesis: ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) )

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) )

reconsider G = GoB f as Go-board ;

1 <= width G by GOBOARD7:33;

then A14: v_strip (G,0) = { |[r1,s]| where r1, s is Real : r1 <= (G * (1,1)) `1 } by GOBOARD5:10;

|[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : r1 <= ((GoB f) * (1,1)) `1 } by A13;

then p in v_strip ((GoB f),0) by A14, EUCLID:53;

hence ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ; :: thesis: verum

end;1 <= width G by GOBOARD7:33;

then A14: v_strip (G,0) = { |[r1,s]| where r1, s is Real : r1 <= (G * (1,1)) `1 } by GOBOARD5:10;

|[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : r1 <= ((GoB f) * (1,1)) `1 } by A13;

then p in v_strip ((GoB f),0) by A14, EUCLID:53;

hence ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ; :: thesis: verum

case A15:
((GoB f) * ((len (GoB f)),1)) `1 <= p `1
; :: thesis: ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) )

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) )

reconsider G = GoB f as Go-board ;

1 <= width G by GOBOARD7:33;

then A16: v_strip (G,(len G)) = { |[r1,s]| where r1, s is Real : (G * ((len G),1)) `1 <= r1 } by GOBOARD5:9;

|[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ((GoB f) * ((len G),1)) `1 <= r1 } by A15;

then p in v_strip ((GoB f),(len (GoB f))) by A16, EUCLID:53;

hence ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ; :: thesis: verum

end;1 <= width G by GOBOARD7:33;

then A16: v_strip (G,(len G)) = { |[r1,s]| where r1, s is Real : (G * ((len G),1)) `1 <= r1 } by GOBOARD5:9;

|[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ((GoB f) * ((len G),1)) `1 <= r1 } by A15;

then p in v_strip ((GoB f),(len (GoB f))) by A16, EUCLID:53;

hence ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ; :: thesis: verum

case A17:
ex j being Nat st

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; :: thesis: ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) )

( 1 <= j & j < len (GoB f) & ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) ; :: thesis: ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) )

reconsider G = GoB f as Go-board ;

consider j being Nat such that

A18: 1 <= j and

A19: j < len (GoB f) and

A20: ( ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) by A17;

A21: |[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A20;

1 <= width G by GOBOARD7:33;

then v_strip (G,j) = { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A18, A19, GOBOARD5:8;

then p in v_strip ((GoB f),j) by A21, EUCLID:53;

hence ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) by A19; :: thesis: verum

end;consider j being Nat such that

A18: 1 <= j and

A19: j < len (GoB f) and

A20: ( ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) by A17;

A21: |[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A20;

1 <= width G by GOBOARD7:33;

then v_strip (G,j) = { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A18, A19, GOBOARD5:8;

then p in v_strip ((GoB f),j) by A21, EUCLID:53;

hence ex j0 being Nat st

( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) by A19; :: thesis: verum

A22: j0 <= len (GoB f) and

A23: x in v_strip ((GoB f),j0) ;

set s = p `2 ;

A24: now :: thesis: ( not p `2 < ((GoB f) * (1,1)) `2 & not ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 implies ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) )

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) )

assume that

A25: not p `2 < ((GoB f) * (1,1)) `2 and

A26: not ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 ; :: thesis: ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 )

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; :: thesis: verum

end;A25: not p `2 < ((GoB f) * (1,1)) `2 and

A26: not ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 ; :: thesis: ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 )

now :: thesis: ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 )

hence
ex j being Nat st ( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 )

reconsider l = width (GoB f) as Nat ;

defpred S_{1}[ Nat] means not ( not $1 = 0 & 1 <= $1 & $1 < width (GoB f) & not ((GoB f) * (1,($1 + 1))) `2 <= p `2 );

1 < width (GoB f) by GOBOARD7:33;

then 1 + 1 <= width (GoB f) by NAT_1:13;

then A27: (1 + 1) - 1 <= l - 1 by XREAL_1:9;

assume A28: for j being Nat holds

( not 1 <= j or not j < width (GoB f) or not ((GoB f) * (1,j)) `2 <= p `2 or not p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; :: thesis: contradiction

A29: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
;

A34: for j being Nat holds S_{1}[j]
from NAT_1:sch 2(A33, A29);

A35: l - 1 < (l - 1) + 1 by XREAL_1:29;

then reconsider l1 = l - 1 as Nat by A27, SPPOL_1:2;

0 < l1 by A27;

hence contradiction by A26, A34, A27, A35; :: thesis: verum

end;defpred S

1 < width (GoB f) by GOBOARD7:33;

then 1 + 1 <= width (GoB f) by NAT_1:13;

then A27: (1 + 1) - 1 <= l - 1 by XREAL_1:9;

assume A28: for j being Nat holds

( not 1 <= j or not j < width (GoB f) or not ((GoB f) * (1,j)) `2 <= p `2 or not p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; :: thesis: contradiction

A29: for k being Nat st S

S

proof

A33:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A30: not ( not k = 0 & 1 <= k & k < width (GoB f) & not ((GoB f) * (1,(k + 1))) `2 <= p `2 ) ; :: thesis: S_{1}[k + 1]

( 1 <= k + 1 & k + 1 < width (GoB f) implies ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 )_{1}[k + 1]
; :: thesis: verum

end;assume A30: not ( not k = 0 & 1 <= k & k < width (GoB f) & not ((GoB f) * (1,(k + 1))) `2 <= p `2 ) ; :: thesis: S

( 1 <= k + 1 & k + 1 < width (GoB f) implies ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 )

proof

hence
S
assume A31:
( 1 <= k + 1 & k + 1 < width (GoB f) )
; :: thesis: ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2

end;now :: thesis: not p `2 < ((GoB f) * (1,((k + 1) + 1))) `2

hence
((GoB f) * (1,((k + 1) + 1))) `2 <= p `2
; :: thesis: verumassume A32:
p `2 < ((GoB f) * (1,((k + 1) + 1))) `2
; :: thesis: contradiction

then k <> 0 by A25, A28, GOBOARD7:33;

then 0 + 1 <= k by NAT_1:13;

hence contradiction by A28, A30, A31, A32, XREAL_1:145; :: thesis: verum

end;then k <> 0 by A25, A28, GOBOARD7:33;

then 0 + 1 <= k by NAT_1:13;

hence contradiction by A28, A30, A31, A32, XREAL_1:145; :: thesis: verum

A34: for j being Nat holds S

A35: l - 1 < (l - 1) + 1 by XREAL_1:29;

then reconsider l1 = l - 1 as Nat by A27, SPPOL_1:2;

0 < l1 by A27;

hence contradiction by A26, A34, A27, A35; :: thesis: verum

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; :: thesis: verum

now :: thesis: ( ( p `2 < ((GoB f) * (1,1)) `2 & ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ) or ( ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 & ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ) or ( ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) & ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ) )end;

then consider i0 being Nat such that ( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ) or ( ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 & ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ) or ( ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) & ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ) )

per cases
( p `2 < ((GoB f) * (1,1)) `2 or ((GoB f) * (1,(width (GoB f)))) `2 <= p `2 or ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ) by A24;

end;

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ) by A24;

case A36:
p `2 < ((GoB f) * (1,1)) `2
; :: thesis: ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) )

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) )

reconsider G = GoB f as Go-board ;

1 <= len G by GOBOARD7:32;

then A37: h_strip (G,0) = { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,1)) `2 } by GOBOARD5:7;

|[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : s1 <= ((GoB f) * (1,1)) `2 } by A36;

then p in h_strip ((GoB f),0) by A37, EUCLID:53;

hence ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ; :: thesis: verum

end;1 <= len G by GOBOARD7:32;

then A37: h_strip (G,0) = { |[r1,s1]| where r1, s1 is Real : s1 <= (G * (1,1)) `2 } by GOBOARD5:7;

|[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : s1 <= ((GoB f) * (1,1)) `2 } by A36;

then p in h_strip ((GoB f),0) by A37, EUCLID:53;

hence ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ; :: thesis: verum

case A38:
((GoB f) * (1,(width (GoB f)))) `2 <= p `2
; :: thesis: ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) )

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) )

reconsider G = GoB f as Go-board ;

1 <= len G by GOBOARD7:32;

then A39: h_strip (G,(width G)) = { |[r1,s1]| where r1, s1 is Real : (G * (1,(width G))) `2 <= s1 } by GOBOARD5:6;

|[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ((GoB f) * (1,(width G))) `2 <= s1 } by A38;

then p in h_strip ((GoB f),(width (GoB f))) by A39, EUCLID:53;

hence ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ; :: thesis: verum

end;1 <= len G by GOBOARD7:32;

then A39: h_strip (G,(width G)) = { |[r1,s1]| where r1, s1 is Real : (G * (1,(width G))) `2 <= s1 } by GOBOARD5:6;

|[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ((GoB f) * (1,(width G))) `2 <= s1 } by A38;

then p in h_strip ((GoB f),(width (GoB f))) by A39, EUCLID:53;

hence ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ; :: thesis: verum

case A40:
ex j being Nat st

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; :: thesis: ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) )

( 1 <= j & j < width (GoB f) & ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) ; :: thesis: ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) )

reconsider G = GoB f as Go-board ;

consider j being Nat such that

A41: 1 <= j and

A42: j < width (GoB f) and

A43: ( ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) by A40;

A44: |[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A43;

1 <= len G by GOBOARD7:32;

then h_strip (G,j) = { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A41, A42, GOBOARD5:5;

then p in h_strip ((GoB f),j) by A44, EUCLID:53;

hence ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) by A42; :: thesis: verum

end;consider j being Nat such that

A41: 1 <= j and

A42: j < width (GoB f) and

A43: ( ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) by A40;

A44: |[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A43;

1 <= len G by GOBOARD7:32;

then h_strip (G,j) = { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A41, A42, GOBOARD5:5;

then p in h_strip ((GoB f),j) by A44, EUCLID:53;

hence ex i0 being Nat st

( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) by A42; :: thesis: verum

A45: i0 <= width (GoB f) and

A46: x in h_strip ((GoB f),i0) ;

reconsider X0 = cell ((GoB f),j0,i0) as set ;

x in (v_strip ((GoB f),j0)) /\ (h_strip ((GoB f),i0)) by A23, A46, XBOOLE_0:def 4;

then A47: x in X0 by GOBOARD5:def 3;

X0 in { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } by A22, A45;

hence x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } by A47, TARSKI:def 4; :: thesis: verum

assume x in union { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } ; :: thesis: x in the carrier of (TOP-REAL 2)

then consider X0 being set such that

A48: ( x in X0 & X0 in { (cell ((GoB f),i,j)) where i, j is Nat : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by TARSKI:def 4;

ex i, j being Nat st

( X0 = cell ((GoB f),i,j) & i <= len (GoB f) & j <= width (GoB f) ) by A48;

hence x in the carrier of (TOP-REAL 2) by A48; :: thesis: verum