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 `

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

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

U2 /\ (U1 \/ U2) = u2
by XBOOLE_1:7, XBOOLE_1:28;
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;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

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