take the empty-yielding ManySortedSet of the non empty set ; :: thesis: not the empty-yielding ManySortedSet of the non empty set is non-empty
thus not the empty-yielding ManySortedSet of the non empty set is non-empty ; :: thesis: verum