:: deftheorem Def25 defines OSFreeGen OSAFREE:def 25 :
for S being locally_directed OrderSortedSign
for X being V2() ManySortedSet of S
for s being Element of S
for b₄ being Subset of ( the Sorts of (FreeOSA X) . s) holds
( b₄ = OSFreeGen (s,X) iff for x being object holds
( x in b₄ iff ex a being object st
( a in X . s & x = ((OSNat_Hom ((ParsedTermsOSA X),(LCongruence X))) . s) . (root-tree [a,s]) ) ) );