:: deftheorem Def6 defines free MSAFREE:def 6 :
for S being non empty non void ManySortedSign
for IT being MSAlgebra over S holds
( IT is free iff ex G being GeneratorSet of IT st G is free );