let S be locally_directed OrderSortedSign; :: thesis: for X being non-empty ManySortedSet of S holds FreeOSA X is osfree
let X be non-empty ManySortedSet of S; :: thesis: FreeOSA X is osfree
take OSFreeGen X ; :: according to OSAFREE:def 3 :: thesis: OSFreeGen X is osfree
thus OSFreeGen X is osfree by Th38; :: thesis: verum