theorem Th31: :: OSAFREE:31

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