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