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 openSubset of (T | A) st p in U holds ex W being openSubset 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 openSubset of (T | A) st p in U holds ex W being openSubset of (T | A) st ( p in W & W c= U & Fr W in f . n ) ) implies A in f .(n + 1) ) )
byA4; :: thesis: verum