let n be Nat; :: thesis: for TM being metrizable TopSpace

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

for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds

ex L being Subset of TM st

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

let TM be metrizable TopSpace; :: thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds

for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds

ex L being Subset of TM st

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

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

ex L being Subset of TM st

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

assume that

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

A2: A misses B ; :: thesis: for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds

ex L being Subset of TM st

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

let H be Subset of TM; :: thesis: ( ind H <= n & TM | H is second-countable & TM | H is finite-ind implies ex L being Subset of TM st

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

assume that

A3: ind H <= n and

A4: ( TM | H is second-countable & TM | H is finite-ind ) ; :: thesis: ex L being Subset of TM st

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

H is finite-ind by A4, TOPDIM_1:18;

then ind H = ind (TM | H) by TOPDIM_1:17;

then consider a, b being Subset of (TM | H) such that

A5: [#] (TM | H) = a \/ b and

a misses b and

A6: ind a <= n - 1 and

A7: ind b <= 0 by A3, A4, Lm3;

[#] (TM | H) c= [#] TM by PRE_TOPC:def 4;

then reconsider aa = a, bb = b as Subset of TM by XBOOLE_1:1;

A8: bb is finite-ind by A4, TOPDIM_1:22;

A9: H = aa \/ bb by A5, PRE_TOPC:def 5;

then A10: bb /\ H = bb by XBOOLE_1:7, XBOOLE_1:28;

( ind b = ind bb & (TM | H) | b = TM | bb ) by A4, METRIZTS:9, TOPDIM_1:22;

then consider L being Subset of TM such that

A11: L separates A,B and

A12: L misses bb by A1, A2, A4, A7, A8, TOPDIM_1:37;

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

( L /\ H misses bb & L /\ H c= H ) by A10, A12, XBOOLE_1:17, XBOOLE_1:76;

then ( aa is finite-ind & L /\ H c= aa ) by A4, A9, TOPDIM_1:22, XBOOLE_1:73;

then ( ind a = ind aa & ind (L /\ H) <= ind aa ) by TOPDIM_1:19, TOPDIM_1:21;

hence ( L separates A,B & ind (L /\ H) <= n - 1 ) by A6, A11, XXREAL_0:2; :: thesis: verum

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

for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds

ex L being Subset of TM st

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

let TM be metrizable TopSpace; :: thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds

for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds

ex L being Subset of TM st

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

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

ex L being Subset of TM st

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

assume that

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

A2: A misses B ; :: thesis: for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds

ex L being Subset of TM st

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

let H be Subset of TM; :: thesis: ( ind H <= n & TM | H is second-countable & TM | H is finite-ind implies ex L being Subset of TM st

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

assume that

A3: ind H <= n and

A4: ( TM | H is second-countable & TM | H is finite-ind ) ; :: thesis: ex L being Subset of TM st

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

H is finite-ind by A4, TOPDIM_1:18;

then ind H = ind (TM | H) by TOPDIM_1:17;

then consider a, b being Subset of (TM | H) such that

A5: [#] (TM | H) = a \/ b and

a misses b and

A6: ind a <= n - 1 and

A7: ind b <= 0 by A3, A4, Lm3;

[#] (TM | H) c= [#] TM by PRE_TOPC:def 4;

then reconsider aa = a, bb = b as Subset of TM by XBOOLE_1:1;

A8: bb is finite-ind by A4, TOPDIM_1:22;

A9: H = aa \/ bb by A5, PRE_TOPC:def 5;

then A10: bb /\ H = bb by XBOOLE_1:7, XBOOLE_1:28;

( ind b = ind bb & (TM | H) | b = TM | bb ) by A4, METRIZTS:9, TOPDIM_1:22;

then consider L being Subset of TM such that

A11: L separates A,B and

A12: L misses bb by A1, A2, A4, A7, A8, TOPDIM_1:37;

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

( L /\ H misses bb & L /\ H c= H ) by A10, A12, XBOOLE_1:17, XBOOLE_1:76;

then ( aa is finite-ind & L /\ H c= aa ) by A4, A9, TOPDIM_1:22, XBOOLE_1:73;

then ( ind a = ind aa & ind (L /\ H) <= ind aa ) by TOPDIM_1:19, TOPDIM_1:21;

hence ( L separates A,B & ind (L /\ H) <= n - 1 ) by A6, A11, XXREAL_0:2; :: thesis: verum