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
A7: 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
A8: 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;
A9: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A10: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in Ind1 . (n + 1) or x in Ind2 . (n + 1) )
assume A11: x in Ind1 . (n + 1) ; :: thesis: x in Ind2 . (n + 1)
reconsider A = x as Subset of T by A11;
( 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 A7, A11;
hence x in Ind2 . (n + 1) by A8, A10; :: thesis: verum

end;

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

end;

A13: S₁[ 0 ] by A7, A8;
for n being Nat holds S₁[n] from NAT_1:sch 2(A13, A9);
hence Ind1 = Ind2 ; :: thesis: verum