:: deftheorem defines osfree OSAFREE:def 3 :
for S being OrderSortedSign
for IT being monotone OSAlgebra of S holds
( IT is osfree iff ex G being OSGeneratorSet of IT st G is osfree );