consider f being Poset-yielding ManySortedSet of I;
take f ; :: thesis: f is Poset-yielding
thus f is Poset-yielding ; :: thesis: verum