consider x being object 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 finite-ind ) ; :: thesis: verum