let T be TopSpace; :: thesis: for A being Subset of T
for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
let A be Subset of T; :: thesis: for G being Subset-Family of T
for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
let G be Subset-Family of T; :: thesis: for Ga being Subset-Family of (T | A) st Ga is finite-ind & Ga = G holds
( G is finite-ind & ind G = ind Ga )
let G1 be Subset-Family of (T | A); :: thesis: ( G1 is finite-ind & G1 = G implies ( G is finite-ind & ind G = ind G1 ) )
assume that
A1: G1 is finite-ind and
A2: G1 = G ; :: thesis: ( G is finite-ind & ind G = ind G1 )
A3: for B being Subset of T st B in G holds
( B is finite-ind & ind B <= ind G1 )

proof

let B be Subset of T; :: thesis: ( B in G implies ( B is finite-ind & ind B <= ind G1 ) )
assume A4: B in G ; :: thesis: ( B is finite-ind & ind B <= ind G1 )
then reconsider B9 = B as Subset of (T | A) by A2;
A5: B9 is finite-ind by A1, A2, A4;
then ind B = ind B9 by Th22;
hence ( B is finite-ind & ind B <= ind G1 ) by A1, A2, A4, A5, Th11, Th22; :: thesis: verum

end;

A6: - 1 <= ind G1 by A1, Th11;
then A7: ind G <= ind G1 by A3, Th11;
A8: G is finite-ind by A3, A6, Th11;
A9: for B being Subset of (T | A) st B in G1 holds
( B is finite-ind & ind B <= ind G )

proof

let B be Subset of (T | A); :: thesis: ( B in G1 implies ( B is finite-ind & ind B <= ind G ) )
assume A10: B in G1 ; :: thesis: ( B is finite-ind & ind B <= ind G )
then reconsider B9 = B as Subset of T by A2;
B9 is finite-ind by A2, A3, A10;
then ind B = ind B9 by Th21;
hence ( B is finite-ind & ind B <= ind G ) by A1, A2, A8, A10, Th11; :: thesis: verum

end;

- 1 <= ind G by A8, Th11;
then ind G1 <= ind G by A9, Th11;
hence ( G is finite-ind & ind G = ind G1 ) by A3, A6, A7, Th11, XXREAL_0:1; :: thesis: verum