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