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 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 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
reconsider l = len (GoB f) as Element of NAT ;
defpred S1[ Element of 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 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
A6: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of 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
A9: 0 <= k by NAT_1:2;
assume A10: p `1 < ((GoB f) * (((k + 1) + 1),1)) `1 ; :: thesis: contradiction
then k <> 0 by A2, A5, GOBOARD7:32;
then 0 + 1 <= k by A9, NAT_1:13;
hence contradiction by A5, A7, A8, A10, 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;
A11: S1[ 0 ] ;
A12: for j being Element of NAT holds S1[j] from NAT_1:sch 1(A11, A6);
A13: l - 1 < (l - 1) + 1 by XREAL_1:29;
then reconsider l1 = l - 1 as Element of NAT by A4, SPPOL_1:2;
0 < l1 by A4;
hence contradiction by A3, A12, A4, 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 <= width G by GOBOARD7:33;
then A15: 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 A14;
then p in v_strip ((GoB f),0) by A15, EUCLID:53;
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 <= width G by GOBOARD7:33;
then A17: 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 A16;
then p in v_strip ((GoB f),(len (GoB f))) by A17, EUCLID:53;
hence ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) ; :: thesis: verum
end;
case A18: 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) )
reconsider G = GoB f as Go-board ;
consider j being Element of NAT such that
A19: 1 <= j and
A20: j < len (GoB f) and
A21: ( ((GoB f) * (j,1)) `1 <= p `1 & p `1 < ((GoB f) * ((j + 1),1)) `1 ) by A18;
A22: |[(p `1),(p `2)]| in { |[r1,s]| where r1, s is Real : ( (G * (j,1)) `1 <= r1 & r1 <= (G * ((j + 1),1)) `1 ) } by A21;
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 A19, A20, GOBOARD5:8;
then p in v_strip ((GoB f),j) by A22, EUCLID:53;
hence ex j0 being Element of NAT st
( j0 <= len (GoB f) & x in v_strip ((GoB f),j0) ) by A20; :: thesis: verum
end;
end;
end;
then consider j0 being Element of NAT such that
A23: j0 <= len (GoB f) and
A24: x in v_strip ((GoB f),j0) ;
set s = p `2 ;
A25: now
assume that
A26: not p `2 < ((GoB f) * (1,1)) `2 and
A27: 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
reconsider l = width (GoB f) as Element of NAT ;
defpred S1[ Element of 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 A28: (1 + 1) - 1 <= l - 1 by XREAL_1:9;
assume A29: 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
A30: for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A31: 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 A32: ( 1 <= k + 1 & k + 1 < width (GoB f) ) ; :: thesis: ((GoB f) * (1,((k + 1) + 1))) `2 <= p `2
now
A33: 0 <= k by NAT_1:2;
assume A34: p `2 < ((GoB f) * (1,((k + 1) + 1))) `2 ; :: thesis: contradiction
then k <> 0 by A26, A29, GOBOARD7:33;
then 0 + 1 <= k by A33, NAT_1:13;
hence contradiction by A29, A31, A32, A34, 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;
A35: S1[ 0 ] ;
A36: for j being Element of NAT holds S1[j] from NAT_1:sch 1(A35, A30);
A37: l - 1 < (l - 1) + 1 by XREAL_1:29;
then reconsider l1 = l - 1 as Element of NAT by A28, SPPOL_1:2;
0 < l1 by A28;
hence contradiction by A27, A36, A28, A37; :: 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 A25;
case A38: 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:32;
then A39: 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 A38;
then p in h_strip ((GoB f),0) by A39, EUCLID:53;
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 A40: ((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 <= len G by GOBOARD7:32;
then A41: 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 A40;
then p in h_strip ((GoB f),(width (GoB f))) by A41, EUCLID:53;
hence ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) ; :: thesis: verum
end;
case A42: 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) )
reconsider G = GoB f as Go-board ;
consider j being Element of NAT such that
A43: 1 <= j and
A44: j < width (GoB f) and
A45: ( ((GoB f) * (1,j)) `2 <= p `2 & p `2 < ((GoB f) * (1,(j + 1))) `2 ) by A42;
A46: |[(p `1),(p `2)]| in { |[r1,s1]| where r1, s1 is Real : ( (G * (1,j)) `2 <= s1 & s1 <= (G * (1,(j + 1))) `2 ) } by A45;
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 A43, A44, GOBOARD5:5;
then p in h_strip ((GoB f),j) by A46, EUCLID:53;
hence ex i0 being Element of NAT st
( i0 <= width (GoB f) & x in h_strip ((GoB f),i0) ) by A44; :: thesis: verum
end;
end;
end;
then consider i0 being Element of NAT such that
A47: i0 <= width (GoB f) and
A48: 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 A24, A48, XBOOLE_0:def 4;
then A49: x in X0 by GOBOARD5:def 3;
X0 in { (cell ((GoB f),i,j)) where i, j is Element of NAT : ( i <= len (GoB f) & j <= width (GoB f) ) } by A23, A47;
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 A49, 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
A50: ( 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 A50;
hence x in the carrier of (TOP-REAL 2) by A50; :: thesis: verum