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 Element of 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 Element of 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 Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } c= the carrier of (TOP-REAL 2)

proof

let x be set ; :: 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 Element of 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 Element of 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

assume A2: ( not p `1 < ((GoB f) * 1,1) `1 & not ((GoB f) * (len (GoB f)),1) `1 <= p `1 ) ; :: thesis: ex j being Element of NAT st
( 1 <= j & j < len (GoB f) & ((GoB f) * j,1) `1 <= p `1 & p `1 < ((GoB f) * (j + 1),1) `1 )

now

assume A3: for j being Element of 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
defpred S₁[ Element of NAT ] means not ( not $1 = 0 & 1 <= $1 & $1 < len (GoB f) & not ((GoB f) * ($1 + 1),1) `1 <= p `1 );
A4: S₁[ 0 ] ;
A5: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: not ( not k = 0 & 1 <= k & k < len (GoB f) & not ((GoB f) * (k + 1),1) `1 <= p `1 ) ; :: thesis: S₁[k + 1]
not ( not k + 1 = 0 & 1 <= k + 1 & k + 1 < len (GoB f) & not ((GoB f) * ((k + 1) + 1),1) `1 <= p `1 )

proof

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

proof

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

now

assume A8: p `1 < ((GoB f) * ((k + 1) + 1),1) `1 ; :: thesis: contradiction
then A9: k <> 0 by A2, A3, GOBOARD7:34;
0 <= k by NAT_1:2;
then 0 + 1 <= k by A9, NAT_1:13;
hence contradiction by A3, A6, A7, A8, XREAL_1:147; :: thesis: verum

end;

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

end;

hence not ( not k + 1 = 0 & 1 <= k + 1 & k + 1 < len (GoB f) & not ((GoB f) * ((k + 1) + 1),1) `1 <= p `1 ) ; :: thesis: verum

end;

hence not ( not k + 1 = 0 & 1 <= k + 1 & k + 1 < len (GoB f) & not ((GoB f) * ((k + 1) + 1),1) `1 <= p `1 ) ; :: thesis: verum

end;

A10: for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A4, A5);
1 < len (GoB f) by GOBOARD7:34;
then A11: 1 + 1 <= len (GoB f) by NAT_1:13;
reconsider l = len (GoB f) as Element of NAT ;
A12: (1 + 1) - 1 <= l - 1 by A11, XREAL_1:11;
A13: l - 1 < (l - 1) + 1 by XREAL_1:31;
then reconsider l1 = l - 1 as Element of NAT by A12, SPPOL_1:7;
0 < l1 by A12;
hence contradiction by A2, A10, A12, A13; :: thesis: verum

end;

hence ex j being Element of NAT st
( 1 <= j & j < len (GoB f) & ((GoB f) * j,1) `1 <= p `1 & p `1 < ((GoB f) * (j + 1),1) `1 ) ; :: thesis: verum

end;

now

per cases ( p `1 < ((GoB f) * 1,1) `1 or ((GoB f) * (len (GoB f)),1) `1 <= p `1 or ex j being Element of 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;

case A14: p `1 < ((GoB f) * 1,1) `1 ; :: thesis: ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip (GoB f),j0 )

reconsider G = GoB f as Go-board ;
( 1 <= 1 & 1 <= width G ) by GOBOARD7:35;
then A15: v_strip G,0 = { |[r1,s]| where r1, s is Real : r1 <= (G * 1,1) `1 } by GOBOARD5:11;
|[(p `1 ),(p `2 )]| in { |[r1,s]| where r1, s is Real : r1 <= ((GoB f) * 1,1) `1 } by A14;
then p in v_strip (GoB f),0 by A15, EUCLID:57;
hence ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip (GoB f),j0 ) by NAT_1:2; :: thesis: verum

end;

case A16: ((GoB f) * (len (GoB f)),1) `1 <= p `1 ; :: thesis: ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip (GoB f),j0 )

reconsider G = GoB f as Go-board ;
( 1 <= 1 & 1 <= width G ) by GOBOARD7:35;
then A17: v_strip G,(len G) = { |[r1,s]| where r1, s is Real : (G * (len G),1) `1 <= r1 } by GOBOARD5:10;
|[(p `1 ),(p `2 )]| in { |[r1,s]| where r1, s is Real : ((GoB f) * (len G),1) `1 <= r1 } by A16;
then p in v_strip (GoB f),(len (GoB f)) by A17, EUCLID:57;
hence ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip (GoB f),j0 ) ; :: thesis: verum

end;

case ex j being Element of 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 Element of NAT st
( j0 <= len (GoB f) & x in v_strip (GoB f),j0 )

then consider j being Element of NAT such that
A18: ( 1 <= j & j < len (GoB f) & ((GoB f) * j,1) `1 <= p `1 & p `1 < ((GoB f) * (j + 1),1) `1 ) ;
reconsider G = GoB f as Go-board ;
( 1 <= 1 & 1 <= width G ) by GOBOARD7:35;
then A19: v_strip G,j = { |[r1,s]| where r1, s is Real : ( (G * j,1) `1 <= r1 & r1 <= (G * (j + 1),1) `1 ) } by A18, GOBOARD5:9;
|[(p `1 ),(p `2 )]| in { |[r1,s]| where r1, s is Real : ( (G * j,1) `1 <= r1 & r1 <= (G * (j + 1),1) `1 ) } by A18;
then p in v_strip (GoB f),j by A19, EUCLID:57;
hence ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip (GoB f),j0 ) by A18; :: thesis: verum

end;

end;

end;

then consider j0 being Element of NAT such that
A20: ( j0 <= len (GoB f) & x in v_strip (GoB f),j0 ) ;
set s = p `2 ;

A21: now

assume A22: ( not p `2 < ((GoB f) * 1,1) `2 & not ((GoB f) * 1,(width (GoB f))) `2 <= p `2 ) ; :: thesis: ex j being Element of NAT st
( 1 <= j & j < width (GoB f) & ((GoB f) * 1,j) `2 <= p `2 & p `2 < ((GoB f) * 1,(j + 1)) `2 )

now

assume A23: for j being Element of 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
defpred S₁[ Element of NAT ] means not ( not $1 = 0 & 1 <= $1 & $1 < width (GoB f) & not ((GoB f) * 1,($1 + 1)) `2 <= p `2 );
A24: S₁[ 0 ] ;
A25: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A26: not ( not k = 0 & 1 <= k & k < width (GoB f) & not ((GoB f) * 1,(k + 1)) `2 <= p `2 ) ; :: thesis: S₁[k + 1]
not ( not k + 1 = 0 & 1 <= k + 1 & k + 1 < width (GoB f) & not ((GoB f) * 1,((k + 1) + 1)) `2 <= p `2 )

proof

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

proof

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

now

assume A28: p `2 < ((GoB f) * 1,((k + 1) + 1)) `2 ; :: thesis: contradiction
then A29: k <> 0 by A22, A23, GOBOARD7:35;
0 <= k by NAT_1:2;
then 0 + 1 <= k by A29, NAT_1:13;
hence contradiction by A23, A26, A27, A28, XREAL_1:147; :: thesis: verum

end;

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

end;

hence not ( not k + 1 = 0 & 1 <= k + 1 & k + 1 < width (GoB f) & not ((GoB f) * 1,((k + 1) + 1)) `2 <= p `2 ) ; :: thesis: verum

end;

hence not ( not k + 1 = 0 & 1 <= k + 1 & k + 1 < width (GoB f) & not ((GoB f) * 1,((k + 1) + 1)) `2 <= p `2 ) ; :: thesis: verum

end;

A30: for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A24, A25);
1 < width (GoB f) by GOBOARD7:35;
then A31: 1 + 1 <= width (GoB f) by NAT_1:13;
reconsider l = width (GoB f) as Element of NAT ;
A32: (1 + 1) - 1 <= l - 1 by A31, XREAL_1:11;
A33: l - 1 < (l - 1) + 1 by XREAL_1:31;
then reconsider l1 = l - 1 as Element of NAT by A32, SPPOL_1:7;
0 < l1 by A32;
hence contradiction by A22, A30, A32, A33; :: thesis: verum

end;

hence ex j being Element of NAT st
( 1 <= j & j < width (GoB f) & ((GoB f) * 1,j) `2 <= p `2 & p `2 < ((GoB f) * 1,(j + 1)) `2 ) ; :: thesis: verum

end;

now

per cases ( p `2 < ((GoB f) * 1,1) `2 or ((GoB f) * 1,(width (GoB f))) `2 <= p `2 or ex j being Element of NAT st
( 1 <= j & j < width (GoB f) & ((GoB f) * 1,j) `2 <= p `2 & p `2 < ((GoB f) * 1,(j + 1)) `2 ) ) by A21;

case A34: p `2 < ((GoB f) * 1,1) `2 ; :: thesis: ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip (GoB f),i0 )

reconsider G = GoB f as Go-board ;
1 <= len G by GOBOARD7:34;
then A35: h_strip G,0 = { |[r1,s1]| where r1, s1 is Real : s1 <= (G * 1,1) `2 } by GOBOARD5:8;
|[(p `1 ),(p `2 )]| in { |[r1,s1]| where r1, s1 is Real : s1 <= ((GoB f) * 1,1) `2 } by A34;
then p in h_strip (GoB f),0 by A35, EUCLID:57;
hence ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip (GoB f),i0 ) by NAT_1:2; :: thesis: verum

end;

case A36: ((GoB f) * 1,(width (GoB f))) `2 <= p `2 ; :: thesis: ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip (GoB f),i0 )

reconsider G = GoB f as Go-board ;
( 1 <= 1 & 1 <= len G ) by GOBOARD7:34;
then A37: h_strip G,(width G) = { |[r1,s1]| where r1, s1 is Real : (G * 1,(width G)) `2 <= s1 } by GOBOARD5:7;
|[(p `1 ),(p `2 )]| in { |[r1,s1]| where r1, s1 is Real : ((GoB f) * 1,(width G)) `2 <= s1 } by A36;
then p in h_strip (GoB f),(width (GoB f)) by A37, EUCLID:57;
hence ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip (GoB f),i0 ) ; :: thesis: verum

end;

case ex j being Element of 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 Element of NAT st
( i0 <= width (GoB f) & x in h_strip (GoB f),i0 )

then consider j being Element of NAT such that
A38: ( 1 <= j & j < width (GoB f) & ((GoB f) * 1,j) `2 <= p `2 & p `2 < ((GoB f) * 1,(j + 1)) `2 ) ;
reconsider G = GoB f as Go-board ;
( 1 <= 1 & 1 <= len G ) by GOBOARD7:34;
then A39: h_strip G,j = { |[r1,s1]| where r1, s1 is Real : ( (G * 1,j) `2 <= s1 & s1 <= (G * 1,(j + 1)) `2 ) } by A38, GOBOARD5:6;
|[(p `1 ),(p `2 )]| in { |[r1,s1]| where r1, s1 is Real : ( (G * 1,j) `2 <= s1 & s1 <= (G * 1,(j + 1)) `2 ) } by A38;
then p in h_strip (GoB f),j by A39, EUCLID:57;
hence ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip (GoB f),i0 ) by A38; :: thesis: verum

end;

end;

end;

then consider i0 being Element of NAT such that
A40: ( i0 <= width (GoB f) & x in h_strip (GoB f),i0 ) ;
A41: x in (v_strip (GoB f),j0) /\ (h_strip (GoB f),i0) by A20, A40, XBOOLE_0:def 4;
reconsider X0 = cell (GoB f),j0,i0 as set ;
( x in X0 & X0 in { (cell (GoB f),i,j) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by A20, A40, A41, GOBOARD5:def 3;
hence x in union { (cell (GoB f),i,j) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by TARSKI:def 4; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in union { (cell (GoB f),i,j) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } or x in the carrier of (TOP-REAL 2) )
assume x in union { (cell (GoB f),i,j) where i, j is Element of 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
A42: ( x in X0 & X0 in { (cell (GoB f),i,j) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } ) by TARSKI:def 4;
ex i, j being Element of NAT st
( X0 = cell (GoB f),i,j & i <= len (GoB f) & j <= width (GoB f) ) by A42;
hence x in the carrier of (TOP-REAL 2) by A42; :: thesis: verum