let n be Nat; :: thesis: for TM being metrizable TopSpace st TM is with_finite_small_inductive_dimension holds
for A being Subset of st ind (A ` ) <= n & TM | (A ` ) is second-countable holds
for A1, A2 being closed Subset of st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
let TM be metrizable TopSpace; :: thesis: ( TM is with_finite_small_inductive_dimension implies for A being Subset of st ind (A ` ) <= n & TM | (A ` ) is second-countable holds
for A1, A2 being closed Subset of st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume A1: TM is with_finite_small_inductive_dimension ; :: thesis: for A being Subset of st ind (A ` ) <= n & TM | (A ` ) is second-countable holds
for A1, A2 being closed Subset of st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
set cTM = [#] TM;
let A be Subset of ; :: thesis: ( ind (A ` ) <= n & TM | (A ` ) is second-countable implies for A1, A2 being closed Subset of st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume that
A2: ind (A ` ) <= n and
A3: TM | (A ` ) is second-countable ; :: thesis: for A1, A2 being closed Subset of st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
let A1, A2 be closed Subset of ; :: thesis: ( A = A1 \/ A2 implies ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume A4: A = A1 \/ A2 ; :: thesis: ex X1, X2 being closed Subset of st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
set A12 = A1 /\ A2;
set T'12 = TM | (([#] TM) \ (A1 /\ A2));
A5: [#] (TM | (([#] TM) \ (A1 /\ A2))) = ([#] TM) \ (A1 /\ A2) by PRE_TOPC:def 10;
A ` c= ([#] TM) \ (A1 /\ A2) by A4, XBOOLE_1:29, XBOOLE_1:34;
then reconsider A1' = A1 \ (A1 /\ A2), A2' = A2 \ (A1 /\ A2), A' = A ` as Subset of by A5, XBOOLE_1:33;
A2 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) = (A2 /\ ([#] TM)) \ (A1 /\ A2) by A5, XBOOLE_1:49
.= A2' by XBOOLE_1:28 ;
then reconsider A2' = A2' as closed Subset of by PRE_TOPC:43;
A1 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) = (A1 /\ ([#] TM)) \ (A1 /\ A2) by A5, XBOOLE_1:49
.= A1' by XBOOLE_1:28 ;
then reconsider A1' = A1' as closed Subset of by PRE_TOPC:43;
A1 \ A2 = A1' by XBOOLE_1:47;
then A1' misses A2 by XBOOLE_1:79;
then A6: A1' misses A2' by XBOOLE_1:36, XBOOLE_1:63;
A7: ind (A ` ) = ind A' by A1, TOPDIM_1:21;
(TM | (([#] TM) \ (A1 /\ A2))) | A' is second-countable by A3, METRIZTS:9;
then consider L being Subset of such that
A8: L separates A1',A2' and
A9: ind (L /\ A') <= n - 1 by A1, A2, A6, A7, Th11;
consider U, W being open Subset of such that
A10: A1' c= U and
A11: A2' c= W and
A12: U misses W and
A13: L = (U \/ W) ` by A8, METRIZTS:def 3;
[#] (TM | (([#] TM) \ (A1 /\ A2))) c= [#] TM by PRE_TOPC:def 9;
then reconsider L' = L, U' = U, W' = W as Subset of by XBOOLE_1:1;
A14: ( A1 = (A1 \ (A1 /\ A2)) \/ (A1 /\ A2) & A2 = (A2 \ (A1 /\ A2)) \/ (A1 /\ A2) ) by XBOOLE_1:17, XBOOLE_1:45;
L misses A

proof

assume L meets A ; :: thesis: contradiction
then consider x being set such that
A15: x in L and
A16: x in A by XBOOLE_0:3;
A17: ( x in A1 or x in A2 ) by A4, A16, XBOOLE_0:def 3;
not x in A1 /\ A2 by A5, A15, XBOOLE_0:def 5;
then ( x in A1' or x in A2' ) by A17, XBOOLE_0:def 5;
then x in U \/ W by A10, A11, XBOOLE_0:def 3;
hence contradiction by A13, A15, XBOOLE_0:def 5; :: thesis: verum

end;

then A18: L = L' \ A by XBOOLE_1:83
.= (L /\ ([#] TM)) \ A by XBOOLE_1:28
.= L /\ A' by XBOOLE_1:49 ;
A19: ([#] TM) \ (([#] TM) \ (A1 /\ A2)) = ([#] TM) /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:28 ;
A20: A1 \ (A1 \ (A1 /\ A2)) = A1 /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:17, XBOOLE_1:28 ;
(A1 /\ A2) ` is open ;
then reconsider U' = U', W' = W' as open Subset of by A5, TSEP_1:9;
take X2 = W' ` ; :: thesis: ex X2 being closed Subset of st
( [#] TM = X2 \/ X2 & A1 c= X2 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X2) \ (A1 /\ A2)) <= n - 1 )
take X1 = U' ` ; :: thesis: ( [#] TM = X2 \/ X1 & A1 c= X2 & A2 c= X1 & A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A21: W' c= X1 by A12, SUBSET_1:43;
A22: W \/ (([#] TM) \ (U \/ W)) = W \/ (X1 /\ X2) by XBOOLE_1:53
.= (W' \/ X1) /\ (W \/ X2) by XBOOLE_1:24
.= (W' \/ X1) /\ ([#] TM) by XBOOLE_1:45
.= X1 /\ ([#] TM) by A21, XBOOLE_1:12
.= X1 by XBOOLE_1:28 ;
thus X2 \/ X1 = ([#] TM) \ (U' /\ W') by XBOOLE_1:54
.= ([#] TM) \ {} by A12, XBOOLE_0:def 7
.= [#] TM ; :: thesis: ( A1 c= X2 & A2 c= X1 & A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A23: U' c= X2 by A12, SUBSET_1:43;
A24: U \/ (([#] TM) \ (U \/ W)) = U \/ (X1 /\ X2) by XBOOLE_1:53
.= (U' \/ X1) /\ (U \/ X2) by XBOOLE_1:24
.= ([#] TM) /\ (U \/ X2) by XBOOLE_1:45
.= ([#] TM) /\ X2 by A23, XBOOLE_1:12
.= X2 by XBOOLE_1:28 ;
([#] TM) \ (([#] TM) \ (A1 /\ A2)) c= ([#] TM) \ (U \/ W) by A5, XBOOLE_1:34;
hence A25: ( A1 c= X2 & A2 c= X1 ) by A10, A11, A14, A19, A24, A22, XBOOLE_1:13; :: thesis: ( A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
then A26: A1 /\ A2 c= A1 /\ X1 by XBOOLE_1:26;
A1 /\ X1 = (([#] TM) /\ A1) \ U' by XBOOLE_1:49
.= A1 \ U' by XBOOLE_1:28 ;
then A1 /\ X1 c= A1 /\ A2 by A10, A20, XBOOLE_1:34;
hence A1 /\ X1 = A1 /\ A2 by A26, XBOOLE_0:def 10; :: thesis: ( A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A27: A2 \ (A2 \ (A1 /\ A2)) = A2 /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:17, XBOOLE_1:28 ;
A28: A1 /\ A2 c= A2 /\ X2 by A25, XBOOLE_1:26;
A2 /\ X2 = (([#] TM) /\ A2) \ W' by XBOOLE_1:49
.= A2 \ W' by XBOOLE_1:28 ;
then A2 /\ X2 c= A1 /\ A2 by A11, A27, XBOOLE_1:34;
hence A1 /\ A2 = X2 /\ A2 by A28, XBOOLE_0:def 10; :: thesis: ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1
(X2 /\ X1) \ (A1 /\ A2) = (([#] TM) \ (W' \/ U')) \ (A1 /\ A2) by XBOOLE_1:53
.= ([#] TM) \ ((W' \/ U') \/ (A1 /\ A2)) by XBOOLE_1:41
.= L by A5, A13, XBOOLE_1:41 ;
hence ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 by A1, A9, A18, TOPDIM_1:21; :: thesis: verum