:: deftheorem defines MinTerms OSAFREE:def 33 :
for S being monotone regular locally_directed OrderSortedSign
for X being V2() ManySortedSet of S holds MinTerms X = rng (PTMin X);