EmptyMS I c= M by PBOOLE:43;
then EmptyMS I is ManySortedSubset of M by PBOOLE:def 18;
then reconsider A = EmptyMS I as Element of Bool M by CLOSURE2:def 1;
take A ; :: thesis: A is finite-yielding
thus A is finite-yielding ; :: thesis: verum