consider M being V3() ManySortedSet of ;
take M ; :: thesis: M is disjoint_valued
thus M is disjoint_valued ; :: thesis: verum