set x = [[0]] I;
[[0]] I c= A by PBOOLE:49;
then reconsider x = [[0]] I as ManySortedSubset of A by PBOOLE:def 23;
take x ; :: thesis: ( x is empty-yielding & x is finite-yielding )
thus ( x is empty-yielding & x is finite-yielding ) ; :: thesis: verum