consider x being set such that
A1: x in [#] T by XBOOLE_0:def 1;
{x} is Subset of T by A1, ZFMISC_1:31;
hence ex b₁ being Subset of T st
( not b₁ is empty & b₁ is with_finite_small_inductive_dimension ) ; :: thesis: verum