let T be TopSpace; :: thesis: ( T is T_1 & T is Lindelof implies ( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds
{} T separates A,B ) )
assume that
A1: T is T_1 and
A2: T is Lindelof ; :: thesis: ( ( T is finite-ind & ind T <= 0 ) iff for A, B being closed Subset of T st A misses B holds
{} T separates A,B )

hereby :: thesis: ( ( for A, B being closed Subset of T st A misses B holds
{} T separates A,B ) implies ( T is finite-ind & ind T <= 0 ) )

assume A3: ( T is finite-ind & ind T <= 0 ) ; :: thesis: for A, B being closed Subset of T st A misses B holds
{} T separates A,B
let A, B be closed Subset of T; :: thesis: ( A misses B implies {} T separates A,B )
assume A misses B ; :: thesis: {} T separates A,B
then consider A9, B9 being closed Subset of T such that
A4: A9 misses B9 and
A5: A9 \/ B9 = [#] T and
A6: ( A c= A9 & B c= B9 ) by A2, A3, Th34;
A7: A9 ` = B9 by A4, A5, PRE_TOPC:5;
( (A9 \/ B9) ` = (({} T) `) ` & A9 = B9 ` ) by A4, A5, PRE_TOPC:5;
hence {} T separates A,B by A4, A6, A7, METRIZTS:def 3; :: thesis: verum

end;

assume A8: for A, B being closed Subset of T st A misses B holds
{} T separates A,B ; :: thesis: ( T is finite-ind & ind T <= 0 )
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 )

proof

let A, B be closed Subset of T; :: thesis: ( A misses B implies ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) )
assume A misses B ; :: thesis: ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 )
then {} T separates A,B by A8;
then consider U, W being open Subset of T such that
A9: ( A c= U & B c= W ) and
A10: U misses W and
A11: {} T = (U \/ W) ` by METRIZTS:def 3;
A12: [#] T = ((U \/ W) `) ` by A11
.= U \/ W ;
then ( U = W ` & W = U ` ) by A10, PRE_TOPC:5;
hence ex A9, B9 being closed Subset of T st
( A9 misses B9 & A9 \/ B9 = [#] T & A c= A9 & B c= B9 ) by A9, A10, A12; :: thesis: verum

end;

hence ( T is finite-ind & ind T <= 0 ) by A1, Th32; :: thesis: verum