for S being monotone regular locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for t1 being Element of TS (DTConOSA X) holds (PTMin X) . ((PTMin X) . t1) = (PTMin X) . t1