consider x being object such that
A1: x in D by XBOOLE_0:def 1;
{x} c= D by A1, ZFMISC_1:31;
then reconsider XX = bool {x} as Subset-Family of D by ZFMISC_1:67;
take XX ; :: thesis: ( XX is finite & XX is with_non-empty_element & XX is subset-closed & XX is finite-membered )
{x} in bool {x} by ZFMISC_1:def 1;
hence ( XX is finite & XX is with_non-empty_element & XX is subset-closed & XX is finite-membered ) ; :: thesis: verum