for S being monotone regular locally_directed OrderSortedSign
for X being V2() ManySortedSet of S holds LCongruence X = PTCongruence X