let TM be metrizable TopSpace; :: thesis: for Null, A being Subset of st TM | Null is second-countable & Null is with_finite_small_inductive_dimension & A is with_finite_small_inductive_dimension & ind Null <= 0 holds
( A \/ Null is with_finite_small_inductive_dimension & ind (A \/ Null) <= (ind A) + 1 )
let Null, A be Subset of ; :: thesis: ( TM | Null is second-countable & Null is with_finite_small_inductive_dimension & A is with_finite_small_inductive_dimension & ind Null <= 0 implies ( A \/ Null is with_finite_small_inductive_dimension & ind (A \/ Null) <= (ind A) + 1 ) )
assume that
A1: TM | Null is second-countable and
A2: Null is with_finite_small_inductive_dimension and
A3: A is with_finite_small_inductive_dimension and
A4: ind Null <= 0 ; :: thesis: ( A \/ Null is with_finite_small_inductive_dimension & ind (A \/ Null) <= (ind A) + 1 )
set TAN = TM | (A \/ Null);
A5: [#] (TM | (A \/ Null)) = A \/ Null by PRE_TOPC:def 10;
then reconsider N' = Null, A' = A as Subset of by XBOOLE_1:7;
A6: ind N' = ind Null by A2, Th21;
( N' is with_finite_small_inductive_dimension & (TM | (A \/ Null)) | N' 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 st b in B holds
N' 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:8;
then reconsider i1 = (ind A) + 1 as Element of NAT by INT_1:16;
A8: ( A' is with_finite_small_inductive_dimension & ind A' = ind A ) by A3, Th21;
A9: for b being Subset of st b in B holds
( Fr b is with_finite_small_inductive_dimension & ind (Fr b) <= i1 - 1 )

proof

let b be Subset of ; :: thesis: ( b in B implies ( Fr b is with_finite_small_inductive_dimension & ind (Fr b) <= i1 - 1 ) )
assume b in B ; :: thesis: ( Fr b is with_finite_small_inductive_dimension & ind (Fr b) <= i1 - 1 )
then N' misses Fr b by A7;
then Fr b c= A' by A5, XBOOLE_1:73;
hence ( Fr b is with_finite_small_inductive_dimension & ind (Fr b) <= i1 - 1 ) by A8, Th19; :: thesis: verum

end;

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