let TM be metrizable TopSpace; :: thesis: for A, B being closed Subset of TM st A misses B holds
for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null )
let A, B be closed Subset of TM; :: thesis: ( A misses B implies for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null ) )
assume A misses B ; :: thesis: for Null being finite-ind Subset of TM st ind Null <= 0 & TM | Null is second-countable holds
ex L being Subset of TM st
( L separates A,B & L misses Null )
then consider U, W being open Subset of TM such that
A1: ( A c= U & B c= W ) and
A2: Cl U misses Cl W by Th2;
let Null be finite-ind Subset of TM; :: thesis: ( ind Null <= 0 & TM | Null is second-countable implies ex L being Subset of TM st
( L separates A,B & L misses Null ) )
assume A3: ( ind Null <= 0 & TM | Null is second-countable ) ; :: thesis: ex L being Subset of TM st
( L separates A,B & L misses Null )
set TN = TM | Null;
A4: [#] (TM | Null) = Null by PRE_TOPC:def 5;
then reconsider Un = (Cl U) /\ Null, Wn = (Cl W) /\ Null as Subset of (TM | Null) by XBOOLE_1:17;
( Un c= Cl U & Wn c= Cl W ) by XBOOLE_1:17;
then A5: Un misses Wn by A2, XBOOLE_1:64;
A6: ind (TM | Null) = ind Null by Lm5;
( Un is closed & Wn is closed ) by A4, TSP_1:def 2;
then {} (TM | Null) separates Un,Wn by A3, A5, A6, Th35;
then consider L being Subset of TM such that
A7: L separates A,B and
A8: Null /\ L c= {} (TM | Null) by A1, A2, METRIZTS:26;
take L ; :: thesis: ( L separates A,B & L misses Null )
Null /\ L = {} by A8;
hence ( L separates A,B & L misses Null ) by A7; :: thesis: verum