let TM be metrizable TopSpace; 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; ( 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 )
; 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; ( 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
; 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 `
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
; ex V2 being open Subset of TM st
( V2 c= U1 & V2 c= U2 & V2 misses V2 & A c= V2 \/ V2 )
take
V1
; ( 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; 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; verum