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:34;
then 1 + 1 <= len (GoB f) by NAT_1:13;
then A4: (1 + 1) - 1 <= l - 1 by XREAL_1:11;
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:34;
then 0 + 1 <= k by A9, NAT_1:13;
hence contradiction by A5, A7, A8, A10, XREAL_1:147; :: 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:31;
then reconsider l1 = l - 1 as Element of NAT by A4, SPPOL_1:7;
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: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 <= 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 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:35;
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:9;
then p in v_strip (GoB f),j by A22, EUCLID:57;
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:35;
then 1 + 1 <= width (GoB f) by NAT_1:13;
then A28: (1 + 1) - 1 <= l - 1 by XREAL_1:11;
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:35;
then 0 + 1 <= k by A33, NAT_1:13;
hence contradiction by A29, A31, A32, A34, XREAL_1:147; :: 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:31;
then reconsider l1 = l - 1 as Element of NAT by A28, SPPOL_1:7;
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:34;
then A39: 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 A38;
then p in h_strip (GoB f),0 by A39, 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 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:34;
then A41: 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 A40;
then p in h_strip (GoB f),(width (GoB f)) by A41, 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 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:34;
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:6;
then p in h_strip (GoB f),j by A46, EUCLID:57;
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