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)
proof
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 ;
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 ) )
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 )
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 )
reconsider l = len (GoB f) as Nat ;
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A7: not ( not k = 0 & 1 <= k & k < len (GoB f) & not ((GoB f) * ((k + 1),1)) `1 <= p `1 ) ; :: thesis: S1[k + 1]
( 1 <= k + 1 & k + 1 < len (GoB f) implies ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 )
proof
assume A8: ( 1 <= k + 1 & k + 1 < len (GoB f) ) ; :: thesis: ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1
now :: thesis: not p `1 < ((GoB f) * (((k + 1) + 1),1)) `1
assume 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;
hence ((GoB f) * (((k + 1) + 1),1)) `1 <= p `1 ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A10: S1[ 0 ] ;
A11: for j being Nat holds S1[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;
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 ) ; :: thesis: verum
end;
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) ) ) )
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;
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) )
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;
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) )
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;
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) )
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;
end;
end;
then consider j0 being Nat such that
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 ) )
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 )
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 )
reconsider l = width (GoB f) as Nat ;
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A30: not ( not k = 0 & 1 <= k & k < width (GoB f) & not ((GoB f) * (1,(k + 1))) `2 <= p `2 ) ; :: thesis: S1[k + 1]
( 1 <= k + 1 & k + 1 < width (GoB f) implies ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 )
proof
assume A31: ( 1 <= k + 1 & k + 1 < width (GoB f) ) ; :: thesis: ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2
now :: thesis: not p `2 < ((GoB f) * (1,((k + 1) + 1))) `2
assume 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;
hence ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2 ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A33: S1[ 0 ] ;
A34: for j being Nat holds S1[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;
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 ) ; :: thesis: verum
end;
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) ) ) )
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;
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) )
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;
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) )
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;
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) )
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;
end;
end;
then consider i0 being Nat such that
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;
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) )
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