for S being non empty non void ManySortedSign
for X being ManySortedSet of the carrier of S
for t being set holds
( ( t in Terminals (DTConMSA X) & X is V5() implies ex s being SortSymbol of S ex x being set st
( x in X . s & t = [x,s] ) ) & ( for s being SortSymbol of S
for x being set st x in X . s holds
[x,s] in Terminals (DTConMSA X) ) )