theorem Th4: :: OSAFREE:4

for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for t being set holds
( t in Terminals (DTConOSA X) iff ex s being Element of S ex x being set st
( x in X . s & t = [x,s] ) )