:: deftheorem defines FreeOSA OSAFREE:def 18 :
for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S holds FreeOSA X = QuotOSAlg ((ParsedTermsOSA X),(LCongruence X));