for S being monotone regular locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for x being set holds
( x is MinTerm of S,X iff x in MinTerms X )