defpred S₁[ object , object ] means ex D1, D2 being set st
( D1 = $1 & D2 = $2 & ( for A being Subset of T holds
( A in D2 iff ( A in D1 or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in D1 ) ) ) ) );
set C = the carrier of T;
reconsider E = {({} T)} as Element of bool (bool the carrier of T) ;
A1: for x being object st x in bool (bool the carrier of T) holds
ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in bool (bool the carrier of T) implies ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] ) )
assume x in bool (bool the carrier of T) ; :: thesis: ex y being object st
( y in bool (bool the carrier of T) & S₁[x,y] )
reconsider xx = x as set by TARSKI:1;
defpred S₂[ object ] means for A being Subset of T holds
( not A = $1 or A in xx or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in xx ) );
consider y being Subset of (bool the carrier of T) such that
A2: for z being set holds
( z in y iff ( z in bool the carrier of T & S₂[z] ) ) from SUBSET_1:sch 1();
take y ; :: thesis: ( y in bool (bool the carrier of T) & S₁[x,y] )
thus y in bool (bool the carrier of T) ; :: thesis: S₁[x,y]
reconsider yy = y as set ;
take xx ; :: thesis: ex D2 being set st
( xx = x & D2 = y & ( for A being Subset of T holds
( A in D2 iff ( A in xx or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in xx ) ) ) ) )
take yy ; :: thesis: ( xx = x & yy = y & ( for A being Subset of T holds
( A in yy iff ( A in xx or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in xx ) ) ) ) )
thus ( xx = x & yy = y ) ; :: thesis: for A being Subset of T holds
( A in yy iff ( A in xx or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in xx ) ) )
let A be Subset of T; :: thesis: ( A in yy iff ( A in xx or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in xx ) ) )
( A in y iff S₂[A] ) by A2;
hence ( A in yy iff ( A in xx or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in xx ) ) ) ; :: thesis: verum

end;

consider p being Function of (bool (bool the carrier of T)),(bool (bool the carrier of T)) such that
A3: for x being object st x in bool (bool the carrier of T) holds
S₁[x,p . x] from FUNCT_2:sch 1(A1);
deffunc H₁( set , set ) -> Element of bool (bool the carrier of T) = p /. $2;
consider f being sequence of (bool (bool the carrier of T)) such that
A4: f . 0 = E and
A5: for n being Nat holds f . (n + 1) = H₁(n,f . n) from NAT_1:sch 12();
reconsider f = f as SetSequence of (bool the carrier of T) ;
take f ; :: thesis: for A being Subset of T
for n being Nat holds
( f . 0 = {({} T)} & ( not A in f . (n + 1) or A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) & ( ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) implies A in f . (n + 1) ) )

now :: thesis: for n being Nat
for A being Subset of T holds
( A in f . (n + 1) iff ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) )

let n be Nat; :: thesis: for A being Subset of T holds
( A in f . (n + 1) iff ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) )
A6: f . (n + 1) = p /. (f . n) by A5
.= p . (f . n) ;
S₁[f . n,p . (f . n)] by A3;
hence for A being Subset of T holds
( A in f . (n + 1) iff ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) ) by A6; :: thesis: verum

end;

hence for A being Subset of T
for n being Nat holds
( f . 0 = {({} T)} & ( not A in f . (n + 1) or A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) & ( ( A in f . n or for p being Point of (T | A)
for U being open Subset of (T | A) st p in U holds
ex W being open Subset of (T | A) st
( p in W & W c= U & Fr W in f . n ) ) implies A in f . (n + 1) ) ) by A4; :: thesis: verum