consider I being set , f being HGrStr-yielding ManySortedSet of I;
take f ; :: thesis: f is HGrStr-yielding
thus f is HGrStr-yielding ; :: thesis: verum