:: deftheorem defines -free MSAFREE4:def 13 :
for S being non empty non void ManySortedSign
for T being EqualSet of S
for A being MSAlgebra over S holds
( A is T -free iff ex G being GeneratorSet of A st G is T -free );