theorem Th80: :: EXCHSORT:80

for x being set holds last <%x%> = x