let Ind1, Ind2 be SetSequence of (bool the carrier of T); :: thesis: ( ( for A being Subset of T
for n being Nat holds
( Ind1 . 0 = {({} T)} & ( not A in Ind1 . (n + 1) or A in Ind1 . 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 Ind1 . n ) ) & ( ( A in Ind1 . 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 Ind1 . n ) ) implies A in Ind1 . (n + 1) ) ) ) & ( for A being Subset of T
for n being Nat holds
( Ind2 . 0 = {({} T)} & ( not A in Ind2 . (n + 1) or A in Ind2 . 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 Ind2 . n ) ) & ( ( A in Ind2 . 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 Ind2 . n ) ) implies A in Ind2 . (n + 1) ) ) ) implies Ind1 = Ind2 )
assume that
A6: for A being Subset of T
for n being Nat holds
( Ind1 . 0 = {({} T)} & ( not A in Ind1 . (n + 1) or A in Ind1 . 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 Ind1 . n ) ) & ( ( A in Ind1 . 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 Ind1 . n ) ) implies A in Ind1 . (n + 1) ) ) and
A7: for A being Subset of T
for n being Nat holds
( Ind2 . 0 = {({} T)} & ( not A in Ind2 . (n + 1) or A in Ind2 . 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 Ind2 . n ) ) & ( ( A in Ind2 . 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 Ind2 . n ) ) implies A in Ind2 . (n + 1) ) ) ; :: thesis: Ind1 = Ind2
defpred S₁[ Nat] means Ind1 . $1 = Ind2 . $1;
A8: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A9: S₁[n] ; :: thesis: S₁[n + 1]
thus Ind1 . (n + 1) c= Ind2 . (n + 1) :: according to XBOOLE_0:def 10 :: thesis: Ind2 . (n + 1) c= Ind1 . (n + 1)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ind1 . (n + 1) or x in Ind2 . (n + 1) )
assume A10: x in Ind1 . (n + 1) ; :: thesis: x in Ind2 . (n + 1)
reconsider A = x as Subset of T by A10;
( A in Ind1 . 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 Ind1 . n ) ) by A6, A10;
hence x in Ind2 . (n + 1) by A7, A9; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Ind2 . (n + 1) or x in Ind1 . (n + 1) )
assume A11: x in Ind2 . (n + 1) ; :: thesis: x in Ind1 . (n + 1)
reconsider A = x as Subset of T by A11;
( A in Ind2 . 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 Ind2 . n ) ) by A7, A11;
hence x in Ind1 . (n + 1) by A6, A9; :: thesis: verum

end;

A12: S₁[ 0 ] by A6, A7;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A12, A8);
hence Ind1 = Ind2 by FUNCT_2:113; :: thesis: verum