let n be Nat; :: thesis: for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable & ind TM <= n holds

for A, B being Subset of TM st A is closed & B is closed & A misses B holds

ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 )

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable & ind TM <= n implies for A, B being Subset of TM st A is closed & B is closed & A misses B holds

ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 ) )

assume that

A1: ( TM is finite-ind & TM is second-countable ) and

A2: ind TM <= n ; :: thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds

ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 )

A3: TM | ([#] TM) is second-countable by A1;

let A, B be Subset of TM; :: thesis: ( A is closed & B is closed & A misses B implies ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 ) )

assume that

A4: ( A is closed & B is closed ) and

A5: A misses B ; :: thesis: ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 )

consider L being Subset of TM such that

A6: ( L separates A,B & ind (L /\ ([#] TM)) <= n - 1 ) by A4, A1, A2, A3, A5, Th11;

take L ; :: thesis: ( L separates A,B & ind L <= n - 1 )

thus ( L separates A,B & ind L <= n - 1 ) by A6, XBOOLE_1:28; :: thesis: verum

for A, B being Subset of TM st A is closed & B is closed & A misses B holds

ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 )

let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind & TM is second-countable & ind TM <= n implies for A, B being Subset of TM st A is closed & B is closed & A misses B holds

ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 ) )

assume that

A1: ( TM is finite-ind & TM is second-countable ) and

A2: ind TM <= n ; :: thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds

ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 )

A3: TM | ([#] TM) is second-countable by A1;

let A, B be Subset of TM; :: thesis: ( A is closed & B is closed & A misses B implies ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 ) )

assume that

A4: ( A is closed & B is closed ) and

A5: A misses B ; :: thesis: ex L being Subset of TM st

( L separates A,B & ind L <= n - 1 )

consider L being Subset of TM such that

A6: ( L separates A,B & ind (L /\ ([#] TM)) <= n - 1 ) by A4, A1, A2, A3, A5, Th11;

take L ; :: thesis: ( L separates A,B & ind L <= n - 1 )

thus ( L separates A,B & ind L <= n - 1 ) by A6, XBOOLE_1:28; :: thesis: verum