:: deftheorem Def32 defines MinTerm OSAFREE:def 32 :
for S being monotone regular locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S
for b₃ being Element of TS (DTConOSA X) holds
( b₃ is MinTerm of S,X iff (PTMin X) . b₃ = b₃ );