reconsider T = {{}} as Tree ;
take T ; :: thesis: T is finite-order
take 0 ; :: according to TREES_2:def 2 :: thesis: for t being Element of T holds not t ^ <*0*> in T
let t be Element of T; :: thesis: not t ^ <*0*> in T
thus not t ^ <*0*> in T by TARSKI:def 1; :: thesis: verum