let x be ManySortedSubset of A; :: thesis: x is finite-yielding
reconsider x9 = x as ManySortedSet of I ;
x9 c= A by PBOOLE:def 23;
hence x is finite-yielding by Th18; :: thesis: verum