[[0]] I c= M by PBOOLE:43;
then [[0]] I is ManySortedSubset of M by PBOOLE:def 18;
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