set M = the V3() ManySortedSet of I;
take the V3() ManySortedSet of I ; :: thesis: the V3() ManySortedSet of I is disjoint_valued
thus the V3() ManySortedSet of I is disjoint_valued ; :: thesis: verum