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