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

proof

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

end;

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

proof

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

end;

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