:: FINTOPO3 semantic presentation

begin


definition
let T be non empty RelStr ;
let A be Subset of T;
funcA ^d  ->  Subset of T equals :: FINTOPO3:def 1
 {  x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y  }  ;
coherence
  {  x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y  }  is Subset of T
proof
defpred S1[ Element of T] means  for y being Element of T st y in A ` holds
not $1 in U_FT y;
  {  x where x is Element of T : S1[x]  }  is Subset of T from DOMAIN_1:sch_7();
hence   {  x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y  }  is Subset of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines ^d FINTOPO3:def_1_:_
 for T being non empty RelStr
for A being Subset of T holds A ^d =  {  x where x is Element of T : for y being Element of T st y in A ` holds
not x in U_FT y  }  ;

theorem Th1: :: FINTOPO3:1
for T being non empty RelStr
for A being Subset of T st T is filled holds
A c= A ^f
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
A c= A ^f
let A be Subset of T; ::_thesis: ( T is filled implies A c= A ^f )
assume A1: T is filled ; ::_thesis: A c= A ^f
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A or x in A ^f )
assume A2: x in A ; ::_thesis: x in A ^f
then reconsider y = x as Element of T ;
 y in U_FT y by A1, FIN_TOPO:def_4;
hence  x in A ^f by A2, FIN_TOPO:11; ::_thesis: verum
end;

theorem Th2: :: FINTOPO3:2
for T being non empty RelStr
for A being Subset of T
for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T
for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
let A be Subset of T; ::_thesis: for x being Element of T holds
( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
let x be Element of T; ::_thesis: ( x in A ^d iff for y being Element of T st y in A ` holds
not x in U_FT y )
thus  ( x in A ^d implies for y being Element of T st y in A ` holds
not x in U_FT y ) ::_thesis: ( ( for y being Element of T st y in A ` holds
not x in U_FT y ) implies x in A ^d )
proof
assume  x in A ^d ; ::_thesis: for y being Element of T st y in A ` holds
not x in U_FT y
then  ex y being Element of T st
( y = x & ( for z being Element of T st z in A ` holds
not y in U_FT z ) ) ;
hence  for y being Element of T st y in A ` holds
not x in U_FT y ; ::_thesis: verum
end;
assume  for z being Element of T st z in A ` holds
not x in U_FT z ; ::_thesis: x in A ^d
hence  x in A ^d ; ::_thesis: verum
end;

theorem Th3: :: FINTOPO3:3
for T being non empty RelStr
for A being Subset of T st T is filled holds
A ^d c= A
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
A ^d c= A
let A be Subset of T; ::_thesis: ( T is filled implies A ^d c= A )
assume A1: T is filled ; ::_thesis: A ^d c= A
thus  A ^d c= A ::_thesis: verum
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in A ^d or x in A )
assume A2: x in A ^d ; ::_thesis: x in A
then reconsider z = x as Element of T ;
now__::_thesis:_x_in_A
assume  not x in A ; ::_thesis: contradiction
then A3: x in A ` by A2, SUBSET_1:29;
 x in U_FT z by A1, FIN_TOPO:def_4;
hence  contradiction by A2, A3, Th2; ::_thesis: verum
end;
hence  x in A ; ::_thesis: verum
end;
end;

theorem Th4: :: FINTOPO3:4
for T being non empty RelStr
for A being Subset of T holds A ^d = ((A `) ^f) `
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds A ^d = ((A `) ^f) `
let A be Subset of T; ::_thesis: A ^d = ((A `) ^f) `
 for x being set holds
( x in A ^d iff x in ((A `) ^f) ` )
proof
let x be set ; ::_thesis: ( x in A ^d iff x in ((A `) ^f) ` )
A1: (A `) ^f =  {  x2 where x2 is Element of T : ex y being Element of T st
( y in A ` & x2 in U_FT y )  }  by FIN_TOPO:def_12;
thus  ( x in A ^d implies x in ((A `) ^f) ` ) ::_thesis: ( x in ((A `) ^f) ` implies x in A ^d )
proof
A2: (A `) ^f =  {  x2 where x2 is Element of T : ex y being Element of T st
( y in A ` & x2 in U_FT y )  }  by FIN_TOPO:def_12;
assume A3: x in A ^d ; ::_thesis: x in ((A `) ^f) `
then  for x2 being Element of T holds
( not x2 = x or for y being Element of T holds
( not y in A ` or not x2 in U_FT y ) ) by Th2;
then  not x in (A `) ^f by A2;
hence  x in ((A `) ^f) ` by A3, SUBSET_1:29; ::_thesis: verum
end;
assume A4: x in ((A `) ^f) ` ; ::_thesis: x in A ^d
then  not x in (A `) ^f by XBOOLE_0:def_5;
then  for y being Element of T st y in A ` holds
not x in U_FT y by A1;
hence  x in A ^d by A4; ::_thesis: verum
end;
hence  A ^d = ((A `) ^f) ` by TARSKI:1; ::_thesis: verum
end;

theorem Th5: :: FINTOPO3:5
for T being non empty RelStr
for A, B being Subset of T st A c= B holds
A ^f c= B ^f
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T st A c= B holds
A ^f c= B ^f
let A, B be Subset of T; ::_thesis: ( A c= B implies A ^f c= B ^f )
assume A1: A c= B ; ::_thesis: A ^f c= B ^f
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A ^f or z in B ^f )
assume  z in A ^f ; ::_thesis: z in B ^f
then  ex y being Element of T st
( y in A & z in U_FT y ) by FIN_TOPO:11;
hence  z in B ^f by A1, FIN_TOPO:11; ::_thesis: verum
end;

theorem Th6: :: FINTOPO3:6
for T being non empty RelStr
for A, B being Subset of T st A c= B holds
A ^d c= B ^d
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T st A c= B holds
A ^d c= B ^d
let A, B be Subset of T; ::_thesis: ( A c= B implies A ^d c= B ^d )
assume  A c= B ; ::_thesis: A ^d c= B ^d
then A1: B ` c= A ` by SUBSET_1:12;
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A ^d or z in B ^d )
assume A2: z in A ^d ; ::_thesis: z in B ^d
then  for y being Element of T st y in B ` holds
not z in U_FT y by A1, Th2;
hence  z in B ^d by A2; ::_thesis: verum
end;

theorem :: FINTOPO3:7
for T being non empty RelStr
for A, B being Subset of T holds (A /\ B) ^b c= (A ^b) /\ (B ^b)
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A /\ B) ^b c= (A ^b) /\ (B ^b)
let A, B be Subset of T; ::_thesis: (A /\ B) ^b c= (A ^b) /\ (B ^b)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^b or x in (A ^b) /\ (B ^b) )
assume A1: x in (A /\ B) ^b ; ::_thesis: x in (A ^b) /\ (B ^b)
then reconsider px = x as Point of T ;
A2: U_FT px meets A /\ B by A1, FIN_TOPO:8;
then  U_FT px meets B by XBOOLE_1:74;
then A3: x in B ^b by FIN_TOPO:8;
 U_FT px meets A by A2, XBOOLE_1:74;
then  x in A ^b by FIN_TOPO:8;
hence  x in (A ^b) /\ (B ^b) by A3, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th8: :: FINTOPO3:8
for T being non empty RelStr
for A, B being Subset of T holds (A \/ B) ^b = (A ^b) \/ (B ^b)
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A \/ B) ^b = (A ^b) \/ (B ^b)
let A, B be Subset of T; ::_thesis: (A \/ B) ^b = (A ^b) \/ (B ^b)
thus  (A \/ B) ^b c= (A ^b) \/ (B ^b) :: according to XBOOLE_0:def_10 ::_thesis: (A ^b) \/ (B ^b) c= (A \/ B) ^b
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A \/ B) ^b or x in (A ^b) \/ (B ^b) )
assume A1: x in (A \/ B) ^b ; ::_thesis: x in (A ^b) \/ (B ^b)
then reconsider px = x as Point of T ;
 U_FT px meets A \/ B by A1, FIN_TOPO:8;
then  ( U_FT px meets A or U_FT px meets B ) by XBOOLE_1:70;
then  ( x in A ^b or x in B ^b ) by FIN_TOPO:8;
hence  x in (A ^b) \/ (B ^b) by XBOOLE_0:def_3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^b) \/ (B ^b) or x in (A \/ B) ^b )
assume A2: x in (A ^b) \/ (B ^b) ; ::_thesis: x in (A \/ B) ^b
then reconsider px = x as Point of T ;
 ( x in A ^b or x in B ^b ) by A2, XBOOLE_0:def_3;
then  ( U_FT px meets A or U_FT px meets B ) by FIN_TOPO:8;
then  U_FT px meets A \/ B by XBOOLE_1:70;
hence  x in (A \/ B) ^b by FIN_TOPO:8; ::_thesis: verum
end;

theorem :: FINTOPO3:9
for T being non empty RelStr
for A, B being Subset of T holds (A ^i) \/ (B ^i) c= (A \/ B) ^i
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^i) \/ (B ^i) c= (A \/ B) ^i
let A, B be Subset of T; ::_thesis: (A ^i) \/ (B ^i) c= (A \/ B) ^i
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^i) \/ (B ^i) or x in (A \/ B) ^i )
assume A1: x in (A ^i) \/ (B ^i) ; ::_thesis: x in (A \/ B) ^i
then reconsider px = x as Point of T ;
 ( x in A ^i or x in B ^i ) by A1, XBOOLE_0:def_3;
then A2: ( U_FT px c= A or U_FT px c= B ) by FIN_TOPO:7;
 ( A c= A \/ B & B c= A \/ B ) by XBOOLE_1:7;
then  U_FT px c= A \/ B by A2, XBOOLE_1:1;
hence  x in (A \/ B) ^i by FIN_TOPO:7; ::_thesis: verum
end;

theorem Th10: :: FINTOPO3:10
for T being non empty RelStr
for A, B being Subset of T holds (A ^i) /\ (B ^i) = (A /\ B) ^i
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^i) /\ (B ^i) = (A /\ B) ^i
let A, B be Subset of T; ::_thesis: (A ^i) /\ (B ^i) = (A /\ B) ^i
thus  (A ^i) /\ (B ^i) c= (A /\ B) ^i :: according to XBOOLE_0:def_10 ::_thesis: (A /\ B) ^i c= (A ^i) /\ (B ^i)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A ^i) /\ (B ^i) or x in (A /\ B) ^i )
assume A1: x in (A ^i) /\ (B ^i) ; ::_thesis: x in (A /\ B) ^i
then reconsider px = x as Point of T ;
 x in B ^i by A1, XBOOLE_0:def_4;
then A2: U_FT px c= B by FIN_TOPO:7;
 x in A ^i by A1, XBOOLE_0:def_4;
then  U_FT px c= A by FIN_TOPO:7;
then  U_FT px c= A /\ B by A2, XBOOLE_1:19;
hence  x in (A /\ B) ^i by FIN_TOPO:7; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (A /\ B) ^i or x in (A ^i) /\ (B ^i) )
assume A3: x in (A /\ B) ^i ; ::_thesis: x in (A ^i) /\ (B ^i)
then reconsider px = x as Point of T ;
A4: U_FT px c= A /\ B by A3, FIN_TOPO:7;
then  U_FT px c= B by XBOOLE_1:18;
then A5: x in B ^i by FIN_TOPO:7;
 U_FT px c= A by A4, XBOOLE_1:18;
then  x in A ^i by FIN_TOPO:7;
hence  x in (A ^i) /\ (B ^i) by A5, XBOOLE_0:def_4; ::_thesis: verum
end;

theorem Th11: :: FINTOPO3:11
for T being non empty RelStr
for A, B being Subset of T holds (A ^f) \/ (B ^f) = (A \/ B) ^f
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^f) \/ (B ^f) = (A \/ B) ^f
let A, B be Subset of T; ::_thesis: (A ^f) \/ (B ^f) = (A \/ B) ^f
 ( A ^f c= (A \/ B) ^f & B ^f c= (A \/ B) ^f ) by Th5, XBOOLE_1:7;
hence  (A ^f) \/ (B ^f) c= (A \/ B) ^f by XBOOLE_1:8; :: according to XBOOLE_0:def_10 ::_thesis: (A \/ B) ^f c= (A ^f) \/ (B ^f)
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in (A \/ B) ^f or z in (A ^f) \/ (B ^f) )
assume  z in (A \/ B) ^f ; ::_thesis: z in (A ^f) \/ (B ^f)
then consider y being Element of T such that
A1: y in A \/ B and
A2: z in U_FT y by FIN_TOPO:11;
percases ( y in A or y in B ) by A1, XBOOLE_0:def_3;
suppose y in A ; ::_thesis: z in (A ^f) \/ (B ^f)
then  z in A ^f by A2, FIN_TOPO:11;
hence  z in (A ^f) \/ (B ^f) by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose y in B ; ::_thesis: z in (A ^f) \/ (B ^f)
then  z in B ^f by A2, FIN_TOPO:11;
hence  z in (A ^f) \/ (B ^f) by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;

theorem Th12: :: FINTOPO3:12
for T being non empty RelStr
for A, B being Subset of T holds (A ^d) /\ (B ^d) = (A /\ B) ^d
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T holds (A ^d) /\ (B ^d) = (A /\ B) ^d
let A, B be Subset of T; ::_thesis: (A ^d) /\ (B ^d) = (A /\ B) ^d
A1: B ^d = ((B `) ^f) ` by Th4;
thus (A ^d) /\ (B ^d) = (((A `) ^f) `) /\ (B ^d) by Th4
.= (((A `) ^f) \/ ((B `) ^f)) ` by A1, XBOOLE_1:53
.= (((A `) \/ (B `)) ^f) ` by Th11
.= (((A /\ B) `) ^f) ` by XBOOLE_1:54
.= (A /\ B) ^d by Th4 ; ::_thesis: verum
end;

definition
let T be non empty RelStr ;
let A be Subset of T;
func Fcl A ->  Function of NAT,(bool the carrier of T) means :Def2: :: FINTOPO3:def 2
( ( for n being Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^b ) & it . 0 = A );
existence
 ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^b ) & b1 . 0 = A )
proof
defpred S1[ set , set , set ] means  for B being Subset of T st B = $2 holds
$3 = B ^b ;
A1: for n being Element of NAT
for x being Subset of T ex y being Subset of T st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y]
let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y]
reconsider C = x as Subset of T ;
 S1[n,x,C ^b ] ;
hence  ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,(bool the carrier of T) st
( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
hence  ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^b ) & b1 . 0 = A ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^b ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^b ) & b2 . 0 = A holds
b1 = b2
proof
let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^b ) & f1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^b ) & f2 . 0 = A implies f1 = f2 )
assume that
A2: for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^b and
A3: f1 . 0 = A and
A4: for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^b and
A5: f2 . 0 = A ; ::_thesis: f1 = f2
defpred S1[ Element of NAT ] means f1 . $1 = f2 . $1;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
reconsider B1 = f1 . n as Subset of T ;
 B1 ^b = f1 . (n + 1) by A2;
hence  S1[n + 1] by A4, A7; ::_thesis: verum
end;
A8: dom f1 = NAT by FUNCT_2:def_1;
then A9: dom f1 = dom f2 by FUNCT_2:def_1;
A10: S1[ 0 ] by A3, A5;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A6);
then  for x being set st x in dom f1 holds
f1 . x = f2 . x by A8;
hence  f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def2 defines Fcl FINTOPO3:def_2_:_
 for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Fcl A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^b ) & b3 . 0 = A ) );

definition
let T be non empty RelStr ;
let A be Subset of T;
let n be Nat;
func Fcl (A,n) ->  Subset of T equals :: FINTOPO3:def 3
(Fcl A) . n;
coherence
 (Fcl A) . n is Subset of T
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
 (Fcl A) . n9 c= the carrier of T ;
hence  (Fcl A) . n is Subset of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines Fcl FINTOPO3:def_3_:_
 for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fcl (A,n) = (Fcl A) . n;

definition
let T be non empty RelStr ;
let A be Subset of T;
func Fint A ->  Function of NAT,(bool the carrier of T) means :Def4: :: FINTOPO3:def 4
( ( for n being Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^i ) & it . 0 = A );
existence
 ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^i ) & b1 . 0 = A )
proof
defpred S1[ set , set , set ] means  for B being Subset of T st B = $2 holds
$3 = B ^i ;
A1: for n being Element of NAT
for x being Subset of T ex y being Subset of T st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y]
let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y]
reconsider C = x as Subset of T ;
 for B being Subset of T st B = x holds
C ^i = B ^i ;
hence  ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,(bool the carrier of T) st
( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
hence  ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^i ) & b1 . 0 = A ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^i ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^i ) & b2 . 0 = A holds
b1 = b2
proof
let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^i ) & f1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^i ) & f2 . 0 = A implies f1 = f2 )
assume that
A2: for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^i and
A3: f1 . 0 = A and
A4: for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^i and
A5: f2 . 0 = A ; ::_thesis: f1 = f2
defpred S1[ Element of NAT ] means f1 . $1 = f2 . $1;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
reconsider B1 = f1 . n as Subset of T ;
 B1 ^i = f1 . (n + 1) by A2;
hence  S1[n + 1] by A4, A7; ::_thesis: verum
end;
A8: dom f1 = NAT by FUNCT_2:def_1;
then A9: dom f1 = dom f2 by FUNCT_2:def_1;
A10: S1[ 0 ] by A3, A5;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A6);
then  for x being set st x in dom f1 holds
f1 . x = f2 . x by A8;
hence  f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines Fint FINTOPO3:def_4_:_
 for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Fint A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^i ) & b3 . 0 = A ) );

definition
let T be non empty RelStr ;
let A be Subset of T;
let n be Nat;
func Fint (A,n) ->  Subset of T equals :: FINTOPO3:def 5
(Fint A) . n;
coherence
 (Fint A) . n is Subset of T
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
 (Fint A) . n9 c= the carrier of T ;
hence  (Fint A) . n is Subset of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines Fint FINTOPO3:def_5_:_
 for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fint (A,n) = (Fint A) . n;

theorem :: FINTOPO3:13
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds Fcl (A,(n + 1)) = (Fcl (A,n)) ^b by Def2;

theorem :: FINTOPO3:14
for T being non empty RelStr
for A being Subset of T holds Fcl (A,0) = A by Def2;

theorem Th15: :: FINTOPO3:15
for T being non empty RelStr
for A being Subset of T holds Fcl (A,1) = A ^b
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fcl (A,1) = A ^b
let A be Subset of T; ::_thesis: Fcl (A,1) = A ^b
 (Fcl A) . 0 = A by Def2;
then  (Fcl A) . (0 + 1) = A ^b by Def2;
hence  Fcl (A,1) = A ^b ; ::_thesis: verum
end;

theorem :: FINTOPO3:16
for T being non empty RelStr
for A being Subset of T holds Fcl (A,2) = (A ^b) ^b
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fcl (A,2) = (A ^b) ^b
let A be Subset of T; ::_thesis: Fcl (A,2) = (A ^b) ^b
 for B being Subset of T st B = (Fcl A) . 1 holds
(Fcl A) . (1 + 1) = B ^b by Def2;
then  Fcl (A,2) = (Fcl (A,1)) ^b
.= (A ^b) ^b by Th15 ;
hence  Fcl (A,2) = (A ^b) ^b ; ::_thesis: verum
end;

theorem Th17: :: FINTOPO3:17
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
let n be Element of NAT ; ::_thesis: Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n))
 for n being Element of NAT holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n)
proof
defpred S1[ Element of NAT ] means (Fcl (A \/ B)) . $1 = ((Fcl A) . $1) \/ ((Fcl B) . $1);
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
(Fcl (A \/ B)) . (k + 1) = (Fcl ((A \/ B),k)) ^b by Def2
.= ((Fcl (A,k)) ^b) \/ ((Fcl (B,k)) ^b) by A2, Th8
.= (Fcl (A,(k + 1))) \/ ((Fcl (B,k)) ^b) by Def2
.= ((Fcl A) . (k + 1)) \/ ((Fcl B) . (k + 1)) by Def2 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(Fcl (A \/ B)) . 0 = A \/ B by Def2
.= ((Fcl A) . 0) \/ B by Def2
.= ((Fcl A) . 0) \/ ((Fcl B) . 0) by Def2 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  for n being Element of NAT holds (Fcl (A \/ B)) . n = ((Fcl A) . n) \/ ((Fcl B) . n) ; ::_thesis: verum
end;
hence  Fcl ((A \/ B),n) = (Fcl (A,n)) \/ (Fcl (B,n)) ; ::_thesis: verum
end;

theorem :: FINTOPO3:18
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds Fint (A,(n + 1)) = (Fint (A,n)) ^i by Def4;

theorem :: FINTOPO3:19
for T being non empty RelStr
for A being Subset of T holds Fint (A,0) = A by Def4;

theorem Th20: :: FINTOPO3:20
for T being non empty RelStr
for A being Subset of T holds Fint (A,1) = A ^i
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fint (A,1) = A ^i
let A be Subset of T; ::_thesis: Fint (A,1) = A ^i
 ( (Fint A) . 0 = A & ( for B being Subset of T st B = (Fint A) . 0 holds
(Fint A) . (0 + 1) = B ^i ) ) by Def4;
hence  Fint (A,1) = A ^i ; ::_thesis: verum
end;

theorem :: FINTOPO3:21
for T being non empty RelStr
for A being Subset of T holds Fint (A,2) = (A ^i) ^i
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fint (A,2) = (A ^i) ^i
let A be Subset of T; ::_thesis: Fint (A,2) = (A ^i) ^i
thus  Fint (A,2) = Fint (A,(1 + 1))
.= (Fint (A,1)) ^i by Def4
.= (A ^i) ^i by Th20 ; ::_thesis: verum
end;

theorem Th22: :: FINTOPO3:22
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n))
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n))
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n))
defpred S1[ Element of NAT ] means (Fint (A /\ B)) . $1 = ((Fint A) . $1) /\ ((Fint B) . $1);
let n be Element of NAT ; ::_thesis: Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n))
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
(Fint (A /\ B)) . (k + 1) = (Fint ((A /\ B),k)) ^i by Def4
.= ((Fint (A,k)) ^i) /\ ((Fint (B,k)) ^i) by A2, Th10
.= (Fint (A,(k + 1))) /\ ((Fint (B,k)) ^i) by Def4
.= ((Fint A) . (k + 1)) /\ ((Fint B) . (k + 1)) by Def4 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(Fint (A /\ B)) . 0 = A /\ B by Def4
.= ((Fint A) . 0) /\ B by Def4
.= ((Fint A) . 0) /\ ((Fint B) . 0) by Def4 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Fint ((A /\ B),n) = (Fint (A,n)) /\ (Fint (B,n)) ; ::_thesis: verum
end;

theorem :: FINTOPO3:23
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds A c= Fcl (A,n)
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds A c= Fcl (A,n)
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds A c= Fcl (A,n) )
defpred S1[ Element of NAT ] means A c= (Fcl A) . $1;
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds A c= Fcl (A,n)
A2: 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  S1[k] ; ::_thesis: S1[k + 1]
then  A ^b c= (Fcl (A,k)) ^b by FIN_TOPO:14;
then A3: A ^b c= Fcl (A,(k + 1)) by Def2;
 A c= A ^b by A1, FIN_TOPO:13;
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: A c= Fcl (A,n)
A4: S1[ 0 ] by Def2;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  A c= Fcl (A,n) ; ::_thesis: verum
end;

theorem :: FINTOPO3:24
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fint (A,n) c= A
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds Fint (A,n) c= A
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fint (A,n) c= A )
defpred S1[ Element of NAT ] means (Fint A) . $1 c= A;
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fint (A,n) c= A
A2: 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  S1[k] ; ::_thesis: S1[k + 1]
then  (Fint (A,k)) ^i c= A ^i by FINTOPO2:1;
then A3: Fint (A,(k + 1)) c= A ^i by Def4;
 A ^i c= A by A1, FIN_TOPO:22;
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: Fint (A,n) c= A
A4: S1[ 0 ] by Def4;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  Fint (A,n) c= A ; ::_thesis: verum
end;

theorem :: FINTOPO3:25
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1))
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1))
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1)) )
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fcl (A,n) c= Fcl (A,(n + 1))
let n be Element of NAT ; ::_thesis: Fcl (A,n) c= Fcl (A,(n + 1))
 ((Fcl A) . n) ^b = Fcl (A,(n + 1)) by Def2;
hence  Fcl (A,n) c= Fcl (A,(n + 1)) by A1, FIN_TOPO:13; ::_thesis: verum
end;

theorem :: FINTOPO3:26
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n)
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n)
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n) )
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fint (A,(n + 1)) c= Fint (A,n)
let n be Element of NAT ; ::_thesis: Fint (A,(n + 1)) c= Fint (A,n)
 ((Fint A) . n) ^i = Fint (A,(n + 1)) by Def4;
hence  Fint (A,(n + 1)) c= Fint (A,n) by A1, FIN_TOPO:22; ::_thesis: verum
end;

theorem Th27: :: FINTOPO3:27
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n)
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T
for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n)
let A be Subset of T; ::_thesis: for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n)
defpred S1[ Element of NAT ] means (Fint ((A `),$1)) ` = Fcl (A,$1);
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
Fcl (A,(k + 1)) = (Fcl (A,k)) ^b by Def2
.= ((((Fint ((A `),k)) `) `) ^i) ` by A2, FIN_TOPO:16
.= (Fint ((A `),(k + 1))) ` by Def4 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(Fint ((A `),0)) ` = (A `) ` by Def4
.= Fcl (A,0) by Def2 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  for n being Element of NAT holds (Fint ((A `),n)) ` = Fcl (A,n) ; ::_thesis: verum
end;

theorem Th28: :: FINTOPO3:28
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds (Fcl ((A `),n)) ` = Fint (A,n)
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T
for n being Element of NAT holds (Fcl ((A `),n)) ` = Fint (A,n)
let A be Subset of T; ::_thesis: for n being Element of NAT holds (Fcl ((A `),n)) ` = Fint (A,n)
let n be Element of NAT ; ::_thesis: (Fcl ((A `),n)) ` = Fint (A,n)
Fint (A,n) = ((Fint (((A `) `),n)) `) `
.= (Fcl ((A `),n)) ` by Th27 ;
hence  (Fcl ((A `),n)) ` = Fint (A,n) ; ::_thesis: verum
end;

theorem :: FINTOPO3:29
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) `
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) `
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) `
let n be Element of NAT ; ::_thesis: (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) `
(Fcl (A,n)) \/ (Fcl (B,n)) = Fcl ((A \/ B),n) by Th17
.= (Fint (((A \/ B) `),n)) ` by Th27 ;
hence  (Fcl (A,n)) \/ (Fcl (B,n)) = (Fint (((A \/ B) `),n)) ` ; ::_thesis: verum
end;

theorem :: FINTOPO3:30
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) `
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) `
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) `
let n be Element of NAT ; ::_thesis: (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) `
(Fint (A,n)) /\ (Fint (B,n)) = Fint ((A /\ B),n) by Th22
.= (Fcl (((A /\ B) `),n)) ` by Th28 ;
hence  (Fint (A,n)) /\ (Fint (B,n)) = (Fcl (((A /\ B) `),n)) ` ; ::_thesis: verum
end;

definition
let T be non empty RelStr ;
let A be Subset of T;
func Finf A ->  Function of NAT,(bool the carrier of T) means :Def6: :: FINTOPO3:def 6
( ( for n being Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^f ) & it . 0 = A );
existence
 ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^f ) & b1 . 0 = A )
proof
defpred S1[ set , set , set ] means  for B being Subset of T st B = $2 holds
$3 = B ^f ;
A1: for n being Element of NAT
for x being Subset of T ex y being Subset of T st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y]
let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y]
reconsider C = x as Subset of T ;
 for B being Subset of T st B = x holds
C ^f = B ^f ;
hence  ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,(bool the carrier of T) st
( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
hence  ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^f ) & b1 . 0 = A ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^f ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^f ) & b2 . 0 = A holds
b1 = b2
proof
let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^f ) & f1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^f ) & f2 . 0 = A implies f1 = f2 )
assume that
A2: for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^f and
A3: f1 . 0 = A and
A4: for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^f and
A5: f2 . 0 = A ; ::_thesis: f1 = f2
defpred S1[ Element of NAT ] means f1 . $1 = f2 . $1;
A6: dom f1 = NAT by FUNCT_2:def_1;
then A7: dom f1 = dom f2 by FUNCT_2:def_1;
 for n being Element of NAT holds S1[n]
proof
let n be Element of NAT ; ::_thesis: S1[n]
A8: 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 A9: S1[k] ; ::_thesis: S1[k + 1]
reconsider B1 = f1 . k as Subset of T ;
 B1 ^f = f1 . (k + 1) by A2;
hence  S1[k + 1] by A4, A9; ::_thesis: verum
end;
A10: S1[ 0 ] by A3, A5;
 for m being Element of NAT holds S1[m] from NAT_1:sch_1(A10, A8);
hence  S1[n] ; ::_thesis: verum
end;
then  for x being set st x in dom f1 holds
f1 . x = f2 . x by A6;
hence  f1 = f2 by A7, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines Finf FINTOPO3:def_6_:_
 for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Finf A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^f ) & b3 . 0 = A ) );

definition
let T be non empty RelStr ;
let A be Subset of T;
let n be Nat;
func Finf (A,n) ->  Subset of T equals :: FINTOPO3:def 7
(Finf A) . n;
coherence
 (Finf A) . n is Subset of T
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
 (Finf A) . n9 c= the carrier of T ;
hence  (Finf A) . n is Subset of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines Finf FINTOPO3:def_7_:_
 for T being non empty RelStr
for A being Subset of T
for n being Nat holds Finf (A,n) = (Finf A) . n;

definition
let T be non empty RelStr ;
let A be Subset of T;
func Fdfl A ->  Function of NAT,(bool the carrier of T) means :Def8: :: FINTOPO3:def 8
( ( for n being Element of NAT
for B being Subset of T st B = it . n holds
it . (n + 1) = B ^d ) & it . 0 = A );
existence
 ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^d ) & b1 . 0 = A )
proof
defpred S1[ set , set , set ] means  for B being Subset of T st B = $2 holds
$3 = B ^d ;
A1: for n being Element of NAT
for x being Subset of T ex y being Subset of T st S1[n,x,y]
proof
let n be Element of NAT ; ::_thesis: for x being Subset of T ex y being Subset of T st S1[n,x,y]
let x be Subset of T; ::_thesis: ex y being Subset of T st S1[n,x,y]
 for B being Subset of T st B = x holds
x ^d = B ^d ;
hence  ex y being Subset of T st S1[n,x,y] ; ::_thesis: verum
end;
 ex f being Function of NAT,(bool the carrier of T) st
( f . 0 = A & ( for n being Element of NAT holds S1[n,f . n,f . (n + 1)] ) ) from RECDEF_1:sch_2(A1);
hence  ex b1 being Function of NAT,(bool the carrier of T) st
( ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^d ) & b1 . 0 = A ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Function of NAT,(bool the carrier of T) st ( for n being Element of NAT
for B being Subset of T st B = b1 . n holds
b1 . (n + 1) = B ^d ) & b1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = b2 . n holds
b2 . (n + 1) = B ^d ) & b2 . 0 = A holds
b1 = b2
proof
let f1, f2 be Function of NAT,(bool the carrier of T); ::_thesis: ( ( for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^d ) & f1 . 0 = A & ( for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^d ) & f2 . 0 = A implies f1 = f2 )
assume that
A2: for n being Element of NAT
for B being Subset of T st B = f1 . n holds
f1 . (n + 1) = B ^d and
A3: f1 . 0 = A and
A4: for n being Element of NAT
for B being Subset of T st B = f2 . n holds
f2 . (n + 1) = B ^d and
A5: f2 . 0 = A ; ::_thesis: f1 = f2
defpred S1[ Element of NAT ] means f1 . $1 = f2 . $1;
A6: for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A7: S1[n] ; ::_thesis: S1[n + 1]
reconsider B1 = f1 . n as Subset of T ;
 B1 ^d = f1 . (n + 1) by A2;
hence  S1[n + 1] by A4, A7; ::_thesis: verum
end;
A8: dom f1 = NAT by FUNCT_2:def_1;
then A9: dom f1 = dom f2 by FUNCT_2:def_1;
A10: S1[ 0 ] by A3, A5;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A10, A6);
then  for x being set st x in dom f1 holds
f1 . x = f2 . x by A8;
hence  f1 = f2 by A9, FUNCT_1:2; ::_thesis: verum
end;
end;

:: deftheorem Def8 defines Fdfl FINTOPO3:def_8_:_
 for T being non empty RelStr
for A being Subset of T
for b3 being Function of NAT,(bool the carrier of T) holds
( b3 = Fdfl A iff ( ( for n being Element of NAT
for B being Subset of T st B = b3 . n holds
b3 . (n + 1) = B ^d ) & b3 . 0 = A ) );

definition
let T be non empty RelStr ;
let A be Subset of T;
let n be Nat;
func Fdfl (A,n) ->  Subset of T equals :: FINTOPO3:def 9
(Fdfl A) . n;
coherence
 (Fdfl A) . n is Subset of T
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
 (Fdfl A) . n9 c= the carrier of T ;
hence  (Fdfl A) . n is Subset of T ; ::_thesis: verum
end;
end;

:: deftheorem  defines Fdfl FINTOPO3:def_9_:_
 for T being non empty RelStr
for A being Subset of T
for n being Nat holds Fdfl (A,n) = (Fdfl A) . n;

theorem :: FINTOPO3:31
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds Finf (A,(n + 1)) = (Finf (A,n)) ^f by Def6;

theorem :: FINTOPO3:32
for T being non empty RelStr
for A being Subset of T holds Finf (A,0) = A by Def6;

theorem Th33: :: FINTOPO3:33
for T being non empty RelStr
for A being Subset of T holds Finf (A,1) = A ^f
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Finf (A,1) = A ^f
let A be Subset of T; ::_thesis: Finf (A,1) = A ^f
 ( (Finf A) . 0 = A & ( for B being Subset of T st B = (Finf A) . 0 holds
(Finf A) . (0 + 1) = B ^f ) ) by Def6;
hence  Finf (A,1) = A ^f ; ::_thesis: verum
end;

theorem :: FINTOPO3:34
for T being non empty RelStr
for A being Subset of T holds Finf (A,2) = (A ^f) ^f
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Finf (A,2) = (A ^f) ^f
let A be Subset of T; ::_thesis: Finf (A,2) = (A ^f) ^f
Finf (A,2) = Finf (A,(1 + 1))
.= (Finf (A,1)) ^f by Def6
.= (A ^f) ^f by Th33 ;
hence  Finf (A,2) = (A ^f) ^f ; ::_thesis: verum
end;

theorem :: FINTOPO3:35
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))
defpred S1[ Element of NAT ] means (Finf (A \/ B)) . $1 = ((Finf A) . $1) \/ ((Finf B) . $1);
let n be Element of NAT ; ::_thesis: Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n))
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
(Finf (A \/ B)) . (k + 1) = (Finf ((A \/ B),k)) ^f by Def6
.= ((Finf (A,k)) ^f) \/ ((Finf (B,k)) ^f) by A2, Th11
.= (Finf (A,(k + 1))) \/ ((Finf (B,k)) ^f) by Def6
.= ((Finf A) . (k + 1)) \/ ((Finf B) . (k + 1)) by Def6 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(Finf (A \/ B)) . 0 = A \/ B by Def6
.= ((Finf A) . 0) \/ B by Def6
.= ((Finf A) . 0) \/ ((Finf B) . 0) by Def6 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Finf ((A \/ B),n) = (Finf (A,n)) \/ (Finf (B,n)) ; ::_thesis: verum
end;

theorem :: FINTOPO3:36
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds A c= Finf (A,n)
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds A c= Finf (A,n)
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds A c= Finf (A,n) )
defpred S1[ Element of NAT ] means A c= (Finf A) . $1;
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds A c= Finf (A,n)
A2: 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  S1[k] ; ::_thesis: S1[k + 1]
then  A ^f c= (Finf (A,k)) ^f by Th5;
then A3: A ^f c= Finf (A,(k + 1)) by Def6;
 A c= A ^f by A1, Th1;
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: A c= Finf (A,n)
A4: S1[ 0 ] by Def6;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  A c= Finf (A,n) ; ::_thesis: verum
end;

theorem :: FINTOPO3:37
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1))
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1))
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1)) )
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Finf (A,n) c= Finf (A,(n + 1))
let n be Element of NAT ; ::_thesis: Finf (A,n) c= Finf (A,(n + 1))
 ((Finf A) . n) ^f = Finf (A,(n + 1)) by Def6;
hence  Finf (A,n) c= Finf (A,(n + 1)) by A1, Th1; ::_thesis: verum
end;

theorem :: FINTOPO3:38
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds Fdfl (A,(n + 1)) = (Fdfl (A,n)) ^d by Def8;

theorem :: FINTOPO3:39
for T being non empty RelStr
for A being Subset of T holds Fdfl (A,0) = A by Def8;

theorem Th40: :: FINTOPO3:40
for T being non empty RelStr
for A being Subset of T holds Fdfl (A,1) = A ^d
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fdfl (A,1) = A ^d
let A be Subset of T; ::_thesis: Fdfl (A,1) = A ^d
 ( (Fdfl A) . 0 = A & ( for B being Subset of T st B = (Fdfl A) . 0 holds
(Fdfl A) . (0 + 1) = B ^d ) ) by Def8;
hence  Fdfl (A,1) = A ^d ; ::_thesis: verum
end;

theorem :: FINTOPO3:41
for T being non empty RelStr
for A being Subset of T holds Fdfl (A,2) = (A ^d) ^d
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T holds Fdfl (A,2) = (A ^d) ^d
let A be Subset of T; ::_thesis: Fdfl (A,2) = (A ^d) ^d
Fdfl (A,2) = Fdfl (A,(1 + 1))
.= (Fdfl (A,1)) ^d by Def8 ;
hence  Fdfl (A,2) = (A ^d) ^d by Th40; ::_thesis: verum
end;

theorem Th42: :: FINTOPO3:42
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
defpred S1[ Element of NAT ] means (Fdfl (A /\ B)) . $1 = ((Fdfl A) . $1) /\ ((Fdfl B) . $1);
let n be Element of NAT ; ::_thesis: Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n))
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
(Fdfl (A /\ B)) . (k + 1) = (Fdfl ((A /\ B),k)) ^d by Def8
.= ((Fdfl (A,k)) ^d) /\ ((Fdfl (B,k)) ^d) by A2, Th12
.= (Fdfl (A,(k + 1))) /\ ((Fdfl (B,k)) ^d) by Def8
.= ((Fdfl A) . (k + 1)) /\ ((Fdfl B) . (k + 1)) by Def8 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
(Fdfl (A /\ B)) . 0 = A /\ B by Def8
.= ((Fdfl A) . 0) /\ B by Def8
.= ((Fdfl A) . 0) /\ ((Fdfl B) . 0) by Def8 ;
then A3: S1[ 0 ] ;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Fdfl ((A /\ B),n) = (Fdfl (A,n)) /\ (Fdfl (B,n)) ; ::_thesis: verum
end;

theorem :: FINTOPO3:43
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fdfl (A,n) c= A
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds Fdfl (A,n) c= A
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fdfl (A,n) c= A )
defpred S1[ Element of NAT ] means (Fdfl A) . $1 c= A;
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fdfl (A,n) c= A
A2: 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  S1[k] ; ::_thesis: S1[k + 1]
then  (Fdfl (A,k)) ^d c= A ^d by Th6;
then A3: Fdfl (A,(k + 1)) c= A ^d by Def8;
 A ^d c= A by A1, Th3;
hence  S1[k + 1] by A3, XBOOLE_1:1; ::_thesis: verum
end;
let n be Element of NAT ; ::_thesis: Fdfl (A,n) c= A
A4: S1[ 0 ] by Def8;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A4, A2);
hence  Fdfl (A,n) c= A ; ::_thesis: verum
end;

theorem :: FINTOPO3:44
for T being non empty RelStr
for A being Subset of T st T is filled holds
for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n)
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T st T is filled holds
for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n)
let A be Subset of T; ::_thesis: ( T is filled implies for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n) )
assume A1: T is filled ; ::_thesis: for n being Element of NAT holds Fdfl (A,(n + 1)) c= Fdfl (A,n)
let n be Element of NAT ; ::_thesis: Fdfl (A,(n + 1)) c= Fdfl (A,n)
 ((Fdfl A) . n) ^d = Fdfl (A,(n + 1)) by Def8;
hence  Fdfl (A,(n + 1)) c= Fdfl (A,n) by A1, Th3; ::_thesis: verum
end;

theorem Th45: :: FINTOPO3:45
for T being non empty RelStr
for A being Subset of T
for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) `
proof
let T be non empty RelStr ; ::_thesis: for A being Subset of T
for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) `
let A be Subset of T; ::_thesis: for n being Element of NAT holds Fdfl (A,n) = (Finf ((A `),n)) `
defpred S1[ Element of NAT ] means (Fdfl A) . $1 = ((Finf (A `)) . $1) ` ;
let n be Element of NAT ; ::_thesis: Fdfl (A,n) = (Finf ((A `),n)) `
A1: 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 A2: S1[k] ; ::_thesis: S1[k + 1]
 (Fdfl A) . (k + 1) = (Fdfl (A,k)) ^d by Def8;
then (Fdfl A) . (k + 1) = ((((Fdfl A) . k) `) ^f) ` by Th4
.= ((Finf (A `)) . (k + 1)) ` by A2, Def6 ;
hence  S1[k + 1] ; ::_thesis: verum
end;
((Finf (A `)) . 0) ` = (A `) ` by Def6
.= A ;
then A3: S1[ 0 ] by Def8;
 for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1);
hence  Fdfl (A,n) = (Finf ((A `),n)) ` ; ::_thesis: verum
end;

theorem :: FINTOPO3:46
for T being non empty RelStr
for A, B being Subset of T
for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
proof
let T be non empty RelStr ; ::_thesis: for A, B being Subset of T
for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
let A, B be Subset of T; ::_thesis: for n being Element of NAT holds (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
let n be Element of NAT ; ::_thesis: (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) `
(Fdfl (A,n)) /\ (Fdfl (B,n)) = Fdfl ((A /\ B),n) by Th42
.= (Finf (((A /\ B) `),n)) ` by Th45 ;
hence  (Fdfl (A,n)) /\ (Fdfl (B,n)) = (Finf (((A /\ B) `),n)) ` ; ::_thesis: verum
end;

definition
let T be non empty RelStr ;
let n be Nat;
let x be Element of T;
func U_FT (x,n) ->  Subset of T equals :: FINTOPO3:def 10
 Finf ((U_FT x),n);
coherence
 Finf ((U_FT x),n) is Subset of T ;
end;

:: deftheorem  defines U_FT FINTOPO3:def_10_:_
 for T being non empty RelStr
for n being Nat
for x being Element of T holds U_FT (x,n) = Finf ((U_FT x),n);

theorem :: FINTOPO3:47
for T being non empty RelStr
for x being Element of T holds U_FT (x,0) = U_FT x by Def6;

theorem :: FINTOPO3:48
for T being non empty RelStr
for x being Element of T
for n being Element of NAT holds U_FT (x,(n + 1)) = (U_FT (x,n)) ^f by Def6;

definition
let S, T be non empty RelStr ;
predS,T are_mutually_symmetric  means :: FINTOPO3:def 11
( the carrier of S = the carrier of T & ( for x being Element of S
for y being Element of T holds
( y in U_FT x iff x in U_FT y ) ) );
symmetry
 for S, T being non empty RelStr st the carrier of S = the carrier of T & ( for x being Element of S
for y being Element of T holds
( y in U_FT x iff x in U_FT y ) ) holds
( the carrier of T = the carrier of S & ( for x being Element of T
for y being Element of S holds
( y in U_FT x iff x in U_FT y ) ) ) ;
end;

:: deftheorem  defines are_mutually_symmetric FINTOPO3:def_11_:_
 for S, T being non empty RelStr holds
( S,T are_mutually_symmetric iff ( the carrier of S = the carrier of T & ( for x being Element of S
for y being Element of T holds
( y in U_FT x iff x in U_FT y ) ) ) );