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