take T = 1TopSp the non empty set ; :: thesis: ( not T is empty & T is with_finite_small_inductive_dimension )
thus ( not T is empty & T is with_finite_small_inductive_dimension ) ; :: thesis: verum