theorem Th38: :: OSAFREE:38

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