for S being non void Signature
for X, Y being V8() ManySortedSet of the carrier of S
for t1 being Term of S,X
for t2 being Term of S,Y st t1 = t2 holds
the_sort_of t1 = the_sort_of t2