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