let TM be metrizable TopSpace; :: thesis: for A being finite-ind Subset of TM st TM | A is second-countable & ind (TM | A) <= 0 holds
for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
let A be finite-ind Subset of TM; :: thesis: ( TM | A is second-countable & ind (TM | A) <= 0 implies for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) )
assume A1: ( TM | A is second-countable & ind (TM | A) <= 0 ) ; :: thesis: for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds
ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
let U1, U2 be open Subset of TM; :: thesis: ( A c= U1 \/ U2 implies ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) )
assume A2: A c= U1 \/ U2 ; :: thesis: ex V1, V2 being open Subset of TM st
( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 )
set U12 = U1 \/ U2;
set TU = TM | (U1 \/ U2);
A3: [#] (TM | (U1 \/ U2)) = U1 \/ U2 by PRE_TOPC:def 5;
then reconsider u1 = U1, u2 = U2, a = A as Subset of (TM | (U1 \/ U2)) by A2, XBOOLE_1:7;
A4: a is finite-ind by TOPDIM_1:21;
A5: u1 ` misses u2 `
proof
assume u1 ` meets u2 ` ; :: thesis: contradiction
then consider z being object such that
A6: z in u1 ` and
A7: z in u2 ` by XBOOLE_0:3;
( not z in U1 & not z in U2 ) by A6, A7, XBOOLE_0:def 5;
hence contradiction by A3, A6, XBOOLE_0:def 3; :: thesis: verum
end;
U2 /\ (U1 \/ U2) = u2 by XBOOLE_1:7, XBOOLE_1:28;
then A8: u2 is open by A3, TSP_1:def 1;
U1 /\ (U1 \/ U2) = u1 by XBOOLE_1:7, XBOOLE_1:28;
then A9: u1 is open by A3, TSP_1:def 1;
A10: ind a = ind A by TOPDIM_1:21;
( ind A <= 0 & (TM | (U1 \/ U2)) | a is second-countable ) by A1, METRIZTS:9, TOPDIM_1:17;
then consider L being Subset of (TM | (U1 \/ U2)) such that
A11: L separates u1 ` ,u2 ` and
A12: ind (L /\ a) <= 0 - 1 by A4, A5, A9, A8, A10, Th11;
consider v1, v2 being open Subset of (TM | (U1 \/ U2)) such that
A13: ( u1 ` c= v1 & u2 ` c= v2 ) and
A14: v1 misses v2 and
A15: L = (v1 \/ v2) ` by A11, METRIZTS:def 3;
reconsider V1 = v1, V2 = v2 as Subset of TM by A3, XBOOLE_1:1;
reconsider V1 = V1, V2 = V2 as open Subset of TM by A3, TSEP_1:9;
take V2 ; :: thesis: ex V2 being open Subset of TM st
( V2 c= U1 & V2 c= U2 & V2 misses V2 & A c= V2 \/ V2 )
take V1 ; :: thesis: ( V2 c= U1 & V1 c= U2 & V2 misses V1 & A c= V2 \/ V1 )
( u1 ` misses v2 & u2 ` misses v1 ) by A13, A14, XBOOLE_1:63;
hence ( V2 c= U1 & V1 c= U2 & V2 misses V1 ) by A14, SUBSET_1:24; :: thesis: A c= V2 \/ V1
L /\ a c= a by XBOOLE_1:17;
then A16: L /\ a is finite-ind by A4, TOPDIM_1:19;
then ind (L /\ a) >= - 1 by TOPDIM_1:5;
then ind (L /\ a) = - 1 by A12, XXREAL_0:1;
then L /\ a is empty by A16;
then L misses a ;
hence A c= V2 \/ V1 by A15, SUBSET_1:24; :: thesis: verum