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 locally-finite )
thus ( x is empty-yielding & x is locally-finite ) ; :: thesis: verum