[0] I c= M by PBOOLE:49;
then [0] I is ManySortedSubset of M by PBOOLE:def 23;
then reconsider A = [0] I as Element of Bool M by CLOSURE2:def 1;
take A ; :: thesis: A is finite-yielding
thus A is finite-yielding ; :: thesis: verum