:: deftheorem defines osfree OSAFREE:def 2 :
for S being OrderSortedSign
for U0 being monotone OSAlgebra of S
for IT being OSGeneratorSet of U0 holds
( IT is osfree iff for U1 being non-empty monotone OSAlgebra of S
for f being ManySortedFunction of IT, the Sorts of U1 ex h being ManySortedFunction of U0,U1 st
( h is_homomorphism U0,U1 & h is order-sorted & h || IT = f ) );