for S being OrderSortedSign
for X being V2() ManySortedSet of S
for o being OperSymbol of S
for x being Element of Args (o,(ParsedTermsOSA X))
for t being Element of TS (DTConOSA X) st t = (Den (o,(ParsedTermsOSA X))) . x holds
LeastSort t = the_result_sort_of o