set x = EmptyMS I;
EmptyMS I c= A by PBOOLE:43;
then reconsider x = EmptyMS I as ManySortedSubset of A by PBOOLE:def 18;
take x ; :: thesis: ( x is empty-yielding & x is finite-yielding )
thus ( x is empty-yielding & x is finite-yielding ) ; :: thesis: verum