:: deftheorem defines free PRELAMB:def 10 :
for IT being non empty typealg holds
( IT is free iff ( ( for x being type of IT holds
( not ( x is left & x is right ) & not ( x is left & x is middle ) & not ( x is right & x is middle ) ) ) & ( for x being type of IT ex Tr being finite DecoratedTree of the carrier of IT st
for Tr1 being finite DecoratedTree of the carrier of IT holds
( Tr1 represents x iff Tr = Tr1 ) ) ) );