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

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

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

end;

assume A8: for A, B being closed Subset of st A misses B holds
{} T separates A,B ; :: thesis: ( T is with_finite_small_inductive_dimension & ind T <= 0 )
for A, B being closed Subset of st A misses B holds
ex A', B' being closed Subset of st
( A' misses B' & A' \/ B' = [#] T & A c= A' & B c= B' )

proof

let A, B be closed Subset of ; :: thesis: ( A misses B implies ex A', B' being closed Subset of st
( A' misses B' & A' \/ B' = [#] T & A c= A' & B c= B' ) )
assume A misses B ; :: thesis: ex A', B' being closed Subset of st
( A' misses B' & A' \/ B' = [#] T & A c= A' & B c= B' )
then {} T separates A,B by A8;
then consider U, W being open Subset of 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:25;
hence ex A', B' being closed Subset of st
( A' misses B' & A' \/ B' = [#] T & A c= A' & B c= B' ) by A9, A10, A12; :: thesis: verum

end;

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