:: deftheorem Def6 defines free FREEALG:def 6 :
for IT being Universal_Algebra holds
( IT is free iff ex G being GeneratorSet of IT st G is free );