let T be TopSpace; :: thesis: for A, B being Subset of T
for F being Subset of (T | A) st F = B & F is finite-ind holds
( B 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 & F is finite-ind holds
( B is finite-ind & ind F = ind B )
let F be Subset of (T | A); :: thesis: ( F = B & F is finite-ind implies ( B is finite-ind & ind F = ind B ) )
assume that
A1: F = B and
A2: F is finite-ind ; :: thesis: ( B is finite-ind & ind F = ind B )
A3: (T | A) | F = T | B by A1, METRIZTS:9;
then A4: B is finite-ind 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 finite-ind & ind F = ind B ) by A2, A3, Th18; :: thesis: verum