set M = the empty-yielding ManySortedSet of I;
take the empty-yielding ManySortedSet of I ; :: thesis: the empty-yielding ManySortedSet of I is disjoint_valued
thus the empty-yielding ManySortedSet of I is disjoint_valued ; :: thesis: verum