let T be TopSpace; :: thesis:
assume A1: ( T is T_1 & ( for A, B being closed Subset of T st A misses B holds
ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) ) ) ; :: thesis:

A2: now :: thesis:

let p be Point of T; :: thesis:
let U be open Subset of T; :: thesis:
assume A3: p in U ; :: thesis:
reconsider P = {p} as Subset of T by A3, ZFMISC_1:31;
not p in U ` by A3, XBOOLE_0:def 5;
then A4: P misses U ` by ZFMISC_1:50;
not T is empty by A3;
then consider A9, B9 being closed Subset of T such that
A5: A9 misses B9 and
A6: A9 \/ B9 = [#] T and
A7: P c= A9 and
A8: U ` c= B9 by A1, A4;
reconsider W = B9 ` as open Subset of T ;
take W = W; :: thesis:
p in P by TARSKI:def 1;
then ( (U `) ` = U & not p in B9 ) by A5, A7, XBOOLE_0:3;
hence ( p in W & W c= U ) by A3, A8, SUBSET_1:12, XBOOLE_0:def 5; :: thesis:
B9 = A9 ` by A5, A6, PRE_TOPC:5;
then Fr B9 = {} T by TOPGEN_1:14;
hence ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by Th6; :: thesis:

end;

then T is finite-ind by Th15;
hence ( T is finite-ind & ind T <= 0 ) by A2, Th16; :: thesis: