:: deftheorem defines finite-order TREES_2:def 2 :
for IT being Tree holds
( IT is finite-order iff ex n being Nat st
for t being Element of IT holds not t ^ <*n*> in IT );