:: deftheorem defines @ OSAFREE:def 19 :
for S being OrderSortedSign
for X being non-empty ManySortedSet of S
for t being Symbol of (DTConOSA X) holds @ t = { [(root-tree t),s1] where s1 is Element of S : ex s being Element of S ex x being set st
( x in X . s & t = [x,s] & s <= s1 ) } ;