theorem Th39: :: OSAFREE:39

for S being locally_directed OrderSortedSign
for X being non-empty ManySortedSet of S holds FreeOSA X is osfree