theorem Th27: :: OSAFREE:27

for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S holds PTCongruence X is monotone