let T be TopSpace; :: thesis: for A, B being Subset of T
for F being Subset of (T | A) st F = B & F is with_finite_small_inductive_dimension holds
( B is with_finite_small_inductive_dimension & ind F = ind B )
let A, B be Subset of T; :: thesis: for F being Subset of (T | A) st F = B & F is with_finite_small_inductive_dimension holds
( B is with_finite_small_inductive_dimension & ind F = ind B )
let F be Subset of (T | A); :: thesis: ( F = B & F is with_finite_small_inductive_dimension implies ( B is with_finite_small_inductive_dimension & ind F = ind B ) )
assume that
A1: F = B and
A2: F is with_finite_small_inductive_dimension ; :: thesis: ( B is with_finite_small_inductive_dimension & ind F = ind B )
A3: (T | A) | F = T | B by A1, METRIZTS:9;
then A4: B is with_finite_small_inductive_dimension by A2, Th18;
ind F = ind ((T | A) | F) by A2, Lm5
.= ind (T | B) by A1, METRIZTS:9
.= ind B by A4, Lm5 ;
hence ( B is with_finite_small_inductive_dimension & ind F = ind B ) by A2, A3, Th18; :: thesis: verum