consider F being TopStruct-yielding ManySortedSet of {} ;
take F ; :: thesis: F is TopStruct-yielding
thus F is TopStruct-yielding ; :: thesis: verum