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