set F = the TopStruct-yielding ManySortedSet of {} ;
take the TopStruct-yielding ManySortedSet of {} ; :: thesis: the TopStruct-yielding ManySortedSet of {} is TopStruct-yielding
thus the TopStruct-yielding ManySortedSet of {} is TopStruct-yielding ; :: thesis: verum