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