let T be TopSpace; :: thesis: for A being Subset of
for G being Subset-Family of st A in G & G is with_finite_small_inductive_dimension holds
A is with_finite_small_inductive_dimension
let A be Subset of ; :: thesis: for G being Subset-Family of st A in G & G is with_finite_small_inductive_dimension holds
A is with_finite_small_inductive_dimension
let G be Subset-Family of ; :: thesis: ( A in G & G is with_finite_small_inductive_dimension implies A is with_finite_small_inductive_dimension )
assume that
A1: A in G and
A2: G is with_finite_small_inductive_dimension ; :: thesis: A is with_finite_small_inductive_dimension
ex n being Nat st G c= (Seq_of_ind T) . n by A2, Def3;
hence A is with_finite_small_inductive_dimension by A1, Def2; :: thesis: verum