let TM be metrizable TopSpace; :: thesis: for Null, A being Subset of TM st TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 holds
( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )
let Null, A be Subset of TM; :: thesis: ( TM | Null is second-countable & Null is finite-ind & A is finite-ind & ind Null <= 0 implies ( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 ) )
assume that
A1: TM | Null is second-countable and
A2: Null is finite-ind and
A3: A is finite-ind and
A4: ind Null <= 0 ; :: thesis: ( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 )
set TAN = TM | (A \/ Null);
A5: [#] (TM | (A \/ Null)) = A \/ Null by PRE_TOPC:def 5;
then reconsider N9 = Null, A9 = A as Subset of (TM | (A \/ Null)) by XBOOLE_1:7;
A6: ind N9 = ind Null by A2, Th21;
( N9 is finite-ind & (TM | (A \/ Null)) | N9 is second-countable ) by A1, A2, Th21, METRIZTS:9;
then consider B being Basis of (TM | (A \/ Null)) such that
A7: for b being Subset of (TM | (A \/ Null)) st b in B holds
N9 misses Fr b by A4, A6, Th39;
set i = ind A;
- 1 <= ind A by A3, Th5;
then (- 1) + 1 <= (ind A) + 1 by XREAL_1:6;
then reconsider i1 = (ind A) + 1 as Element of NAT by INT_1:3;
A8: ( A9 is finite-ind & ind A9 = ind A ) by A3, Th21;
A9: for b being Subset of (TM | (A \/ Null)) st b in B holds
( Fr b is finite-ind & ind (Fr b) <= i1 - 1 )

proof

let b be Subset of (TM | (A \/ Null)); :: thesis: ( b in B implies ( Fr b is finite-ind & ind (Fr b) <= i1 - 1 ) )
assume b in B ; :: thesis: ( Fr b is finite-ind & ind (Fr b) <= i1 - 1 )
then N9 misses Fr b by A7;
then Fr b c= A9 by A5, XBOOLE_1:73;
hence ( Fr b is finite-ind & ind (Fr b) <= i1 - 1 ) by A8, Th19; :: thesis: verum

end;

then TM | (A \/ Null) is finite-ind by Th31;
then A10: A \/ Null is finite-ind by Th18;
ind (TM | (A \/ Null)) <= i1 by A9, Th31;
hence ( A \/ Null is finite-ind & ind (A \/ Null) <= (ind A) + 1 ) by A10, Lm5; :: thesis: verum