set f = the Poset-yielding ManySortedSet of I;
take the Poset-yielding ManySortedSet of I ; :: thesis: the Poset-yielding ManySortedSet of I is Poset-yielding
thus the Poset-yielding ManySortedSet of I is Poset-yielding ; :: thesis: verum